text:
(**
Rainbow, a termination proof certification tool

See the COPYRIGHTS and LICENSE files.

- Kim Quyen LY, 2011-04-06

* CPF correctness checker

 TO BE FINISH: proving relative termination
*)

Set Implicit Arguments.

Require Import ATrs SN ZArith EqUtil String List ListDec ListForall
  ListUtil ZUtil LogicUtil BoolUtil VecUtil NArith RelUtil RelMidex
  ARelation NatUtil ListExtras RelUtil AVarCond OrdSemiRing2 Polynom2
  MonotonePolynom2 PositivePolynom2 AMannaNess ARedPair2 APolyInt2
  error_monad cpf2color AWFMInterpretation cpf Z_as_SR
  rainbow_full_termin.

Section Top.

  (* We assume given a function translating variable names into
     natural numbers. *)

  Variable nat_of_string : string -> nat.

  (* We assume given an arity function. *)

  Variable arity : symbol -> nat.

  Notation Sig := (Sig arity).
  Notation aterm := (aterm arity).
  Notation arule := (arule arity).
  Notation arules := (arules arity).
  Notation abrule := (abrule arity).

  Implicit Type R : arules.

  (************************************************************************)
  (** Relative termination use polynomial interpretation over
          domain natural and rational numbers.
          Given a pair (>=, >) is a reduction pair.
          if the orders are weakly decreasing in R and D,
          then remove all strictly decreasing in R and D,
          otherwise return error message. *)

  Definition rel_polynomial_interpretation (R D: arules) is dom :
    result arules :=
    match type_polynomial arity is dom with
      | Ok (bge, bgt) =>
        if   ge_R_D R D bge
        then gt_D D bgt (* FIXME : remove R D *)
        else Ko _ (Fail FRuleNotInLargeOrdering_poly)
      | Ko e => Ko _ e
    end.

    (**************************************************************************)
    (** ** Matrix interpretation over domain natural number *)

    Require Import AMatrixBasedInt2 Matrix2 OrdSemiRing2 AMatrixInt2 Nat_as_OSR.

    Open Scope nat_scope.

    (***********************************************************************)
    (** Relative termination use matrix interpretation over domain
       natural numbers. Relative termination has the same condition
       like full termination, where the relation [>] is closed by
       context and [>] is monotone. Use the [type_matrix_polynomial]
       of full termination for relative termination. *)

    Definition rel_matrix_interpretation (R D: arules) is dom dim :=
      match type_matrix arity is dom dim with
        | Ok (bge, bgt) =>
          if   ge_R_D R D bge
          then gt_D D bgt
          else Ko _ (Error ERuleNotInLargeOrdering_matrix_rel)
        | Ko e => Ko _ e
      end.

    Close Scope nat_scope.

    (**********************************************************************)
    (** [type_matrixInterpertation] of relative termination proof.
       REMARK: In domain arctic only occur at top termination and not
       in relative termination. Domain naturals. *)

    Definition rel_type_matrix_interpretation (R D: arules) is dom dim :=
      match dom with
        | Domain_naturals => rel_matrix_interpretation R D is dom
                            (nat_of_P dim)
        | Domain_integers =>
          Ko _ (Todo Ttype_polynomialDomain_integers)
        | Domain_rationals delta =>
          Ko _ (Todo Ttype_polynomialDomain_rationals)
        | Domain_tropical _ =>
          Ko _ (Todo Ttype_polynomialDomain_tropical)
        | Domain_arctic dom'=>
          Ko _ (Todo Ttype_polynomialDomain_arctic)
        | Domain_matrices dim sdim dom' =>
          Ko _ (Todo Ttype_polynomialDomain_matrices)
      end.

    (***********************************************************************)
    (** ** Relative termination reduction pair interpretation with
     polynomial and matrix interpretation in domain: natural numbers
     and rational numbers. *)

    Definition rel_redPair_interpretation (R D: arules) (t: type_t9)
      (is: list (symbol * cpf.arity * function)): result arules :=
      match t with
        | Type_t9_polynomial dom degmax =>
            rel_polynomial_interpretation R D is dom
        | Type_t9_matrixInterpretation dom dim sdim =>
            rel_type_matrix_interpretation R D is dom dim
      end.

    (** Correctness proof of relation redPair interpretation.

      Proof structure:

       1. Correctness proof of polynomial interpretation.

          a. Domain natural numbers.

          b. Domain rational numbers
            - Coefficients are of domain integer.
            - Coefficients are of domain rationals
       2. Correctness proof of matrix interpretation.

          a. Domain natural numbers.

          b. Domain tropical numbers. *)

    Require Import APolyInt_MA2. Import OR_Notations.

    Lemma rel_poly_nat_ok : forall (R D D': arules) is
      (h:  match poly_nat arity is with
            | Ok (bge, bgt) =>
             if   ge_R_D R D bge
             then gt_D D bgt
             else Ko _ (Fail FRuleNotInLargeOrdering_poly)
            | Ko e => Ko _ e
           end = Ok D')(wf: WF (red_mod R D')), WF (red_mod R D).

    Proof.
      intros R D D' is h wf.
      case_eq (poly_nat arity is); intros p H; rewrite H in h; try discr.
      destruct p as [bge bgt].
      case_eq (ge_R_D R D bge);
        intros H0; rewrite H0 in h; try discr.
      unfold gt_D in h. unfold ge_R_D in H0.
      inversion h. subst D'. clear h. simpl in *.
      unfold poly_nat in H. revert H.
      destruct (map_rev (color_interpret arity) is); intros; try discr.
      case_eq (conditions_poly_nat arity l); intro H1;
      rewrite H1 in H; try discr.
      inversion H. clear H.
      unfold conditions_poly_nat in H1.
      set (trsInt := (fun f: symbol => fun_of_pairs_list arity f l)).
      cut (forall f: Sig, pweak_monotone (trsInt f)).
      intros trsInt_wm. Focus 2.
      (** Polynomial weak is monotone. *)
      intro f. apply trsInt_wm_poly.
      (** Proving wellfound of [red_mod]. *)
      rewrite andb_eq in H1. destruct H1. hyp.
      rewrite andb_eq in H1. destruct H1.
      apply WF_rp_red_mod with (WP:=@WP _ _ l H).
      (** Relation [>] is closed by context. *)
      change (context_closed (IR (@I Sig  _ (TPolyInt_poly arity l H)) succ)).
      apply IR_context_closed. apply pi_monotone.
      simpl. intro f.
      (** Polynomial is strong monotone. *)
      apply trsInt_pw_poly. rewrite andb_eq. split. hyp. hyp.
      (** Check that all rules [R] are included in [>=]. *)
      simpl; unfold brule, bsucceq, bool_of_rel; simpl.
      rewrite forallb_forall. intros x Hx. subst bge.
      rewrite andb_eq in H0. destruct H0.
      rewrite forallb_forall in H2.
      ded (H2 x Hx).
      destruct x as [t u]. simpl in *.
      destruct succeq'_dec; try discr; auto.
      unfold succeq' in n. unfold brule, redpair_poly_nat_ge in H3.
      rewrite bcoef_not_neg_ok in H3. contradiction.
      (** All relation [>=] are including in rule [dp R = D]. *)
      simpl; unfold brule, bsucceq, bool_of_rel; simpl.
      rewrite forallb_forall. intros x Hx. subst bge.
      rewrite andb_eq in H0. destruct H0.
      rewrite forallb_forall in H0. ded (H0 x Hx).
      destruct x as [t u]. simpl in *.
      destruct succeq'_dec; auto.
      unfold brule, redpair_poly_nat_ge in H3. rewrite bcoef_not_neg_ok in H3.
      unfold succeq' in n. contradiction.
      (** Remove all rules [D] that are included in [>]. *)
      apply WF_incl with (S:= red_mod (filter (brule (neg bgt)) R)
                                      (filter (brule (neg bgt)) D)).
      unfold inclusion. intros t u H7. redtac. unfold red_mod.
      unfold compose. exists t0. split. simpl in *.
      Focus 2.
      (* red (filter (brule (neg bgt)) D) t0 u *)
      unfold red. exists l0. exists r. exists c.
      exists s. intuition. apply filter_In.
      apply filter_In in lr. intuition.
      unfold brule, neg. unfold brule, neg in H6.
      simpl in *. unfold bsucc, bool_of_rel in H6.
      destruct AMonAlg2.ma_succ'_dec in H6; try discr.
      simpl in *. unfold succ' in n.
      rewrite <- bcoef_not_neg_ok in n.
      apply eq_true_not_negb in n.
      subst bgt. apply n.
      (* red (filter (brule (neg bgt)) R #) t t0 *)
      (* TODO *)

    Admitted.

    (***************************************************************************)
    (** Correctness proof of termination relation [red_mod R D] of
    polynomial interpretation over rational numbers.  *)

    (* REMARK: open scope Q to be able to fold argument [b] in the
    proof. *)

    Open Scope Q_scope. Require Import Q_as_R.

    Lemma rel_poly_rationals_common_ok : forall del (R D D': arules) is
      (h : match poly_rat arity is del with
             | Ok (bge, bgt) =>
               if   ge_R_D R D bge
               then gt_D D bgt
               else Ko _ (Fail FRuleNotInLargeOrdering_poly)
             | Ko e => Ko _ e
           end = Ok D')(wf : WF (red_mod R D')), WF (red_mod R D).

    Proof.
      intros del R D D' is h wf.
      case_eq (poly_rat arity is del); intros p H; rewrite H in h;
      try discr.
      destruct p as [bge bgt].
      case_eq (ge_R_D R D bge);
        intros H0; rewrite H0 in h; try discr.
      unfold gt_D in h. unfold ge_R_D in H0.
      inversion h. subst D'. clear h.
      unfold poly_rat in H.
      case_eq (map_rev (color_interpret arity) is);
        intros l H1; rewrite H1 in H; try discr.
      case_eq (conditions_poly_rat arity l); intros H2; rewrite H2 in H;
      try discr.
      inversion H. clear H.
      unfold conditions_poly_rat in H2.
      set (trsInt := (fun f: symbol => fun_of_pairs_list arity f l)).
      cut (forall f: symbol, pweak_monotone (trsInt f)).
      intros trsInt_wm. Focus 2.
      (** Polynomial weak is monotone. *)
      intro f. apply trsInt_wm_poly.
      (** Proving [WF (red_mod R D)]. *)
      rewrite andb_eq in H2. destruct H2. hyp.
      rewrite andb_eq in H2. destruct H2.
      apply WF_rp_red_mod with (WP:=@WP_Q _ _ l H del).
      (* A proof of [>] are closed by context: IR_context_closed. *)
      change (context_closed (IR (@I Sig _ (TPolyInt_poly arity l H)) succ)).
      apply IR_context_closed. apply pi_monotone.
      simpl. intro f.
      (* Polynomial is strong monotone. *)
      apply trsInt_pw_poly. rewrite andb_eq. split. hyp. hyp.
      (* Check that all rules [R] are included in [>=]. *)
      simpl; unfold brule, ds_wr_bsucceq, bsucceq, bool_of_rel; simpl.
      rewrite forallb_forall. intros x Hx. subst bge.
      rewrite andb_eq in H0. destruct H0.
      rewrite forallb_forall in H3. ded (H3 x Hx). destruct x as [t u].
      simpl in *.
      case_eq (succeq'_dec Sig (TPolyInt_poly arity l H) t u);
        intros s Hs. auto.
      unfold brule, redpair_poly_rat_ge in H4. unfold succeq' in s.
      rewrite bcoef_not_neg_ok in H4. contradiction.
      (** Proving the relation [>=] are in rules [D]. *)
      simpl. unfold brule, bsucceq, bool_of_rel; simpl.
      rewrite forallb_forall. intros x Hx. subst bge.
      rewrite andb_eq in H0. destruct H0.
      rewrite forallb_forall in H0. ded (H0 x Hx).
      destruct x as [t u]. simpl in *.
      case_eq (succeq'_dec Sig (TPolyInt_poly arity l H) t u);
        intros s Hs. auto. unfold brule, redpair_poly_rat_ge in H4.
      unfold succeq' in s.
      rewrite bcoef_not_neg_ok in H4. contradiction.
      (** Proving [red_mod] is well founded when remove all relation
      [>] in [R] and [D]. *)
      apply WF_incl with (S := red_mod (List.filter (brule (neg bgt)) R)
                                       (List.filter (brule (neg bgt)) D)).
      unfold inclusion. intros t u H7. redtac. unfold red_mod.
      unfold compose. exists t0. split. simpl in *.
      Focus 2.
      (* red (filter (brule (neg bgt)) D) t0 u *)
      unfold red. exists l0. exists r. exists c. exists s.
      intuition. apply filter_In.
      apply filter_In in lr. intuition.
      unfold brule, neg. unfold brule, neg in H7.
      simpl in *. unfold bsucc, bool_of_rel in H7.
      destruct AMonAlg2.ma_succ'_dec in H7; try discr.
      simpl in *. unfold succQ' in n.
      rewrite <- bcoef_not_neg_ok in n.
      apply eq_true_not_negb in n.
      subst bgt. apply n.
    (* red (filter (brule (neg bgt)) R #) t t0 *)
    (* TODO *)
    Admitted.

    (**************************************************************************)
    (** Correctness proof of termination relation [red_mod R D] of
    polynomial interpretation over rational numbers.  *)

    Require Import QArith_base.

    Lemma rel_poly_rationals_ok: forall (R D D': arules) is n
      (h:  match type_poly_rationals arity n is with
             | Ok (bge, bgt) =>
               if   ge_R_D R D bge
               then gt_D D bgt
               else Ko _ (Fail FRuleNotInLargeOrdering_poly)
             | Ko e => Ko _ e
           end = Ok D')(wf: WF (red_mod R D')), WF (red_mod R D).

    Proof.
      intros R D D' is n h wf.
      unfold type_poly_rationals in h.
      destruct n; simpl in h; try discr.
      set (del:= inject_Z i). fold del in h.
      (** In the case of rationals -> natural numbers, where it convert a
       natural number to rational number by divide by 1. *)
      apply rel_poly_rationals_common_ok with (del:=del)(D':=D')(is:=is).
      hyp. hyp.
      (** In the case of rationals -> rational numbers. *)
      set (t:= Qmake i p). fold t in h.
      apply rel_poly_rationals_common_ok with (del:=t)(D':=D')(is:=is).
      hyp. hyp.
    Qed.

    Close Scope Q_scope.

    (**************************************************************************)
    (** Correctness proof of termination relation [red_mod R D] of
    polynomial interpretation over rational numbers.  *)

    Lemma rel_polynomial_interpretation_ok: forall (R D D': arules) is d
      (h: rel_polynomial_interpretation R D is d = Ok D')
      (wf : WF (red_mod R D')), WF (red_mod R D).

    Proof.
      intros R D D' is d h wf.
      unfold rel_polynomial_interpretation in h.
      unfold type_polynomial in h.
      destruct d; simpl in h; try discr.
      (** Domain naturals. *)
      apply rel_poly_nat_ok with (D':=D')(is:=is).
      hyp. hyp.
      (** Domain rationals. *)
      apply rel_poly_rationals_ok with (D':=D')(is:=is)(n:=n).
      hyp. hyp.
    Qed.

    (*************************************************************************)
    (** Correctness proof of termination relation [red_mod R D] of
    matrix interpretation of domain natural. *)

    Require Import ABterm OrdSemiRing2.

    Open Scope nat_scope.

    Lemma rel_matrix_interpretation_nat_ok : forall (R D D': arules) d is
      (h: rel_matrix_interpretation R D is Domain_naturals (Pos.to_nat d) =Ok D')
      (wf : WF (red_mod R D')), WF (red_mod R D).

    Proof.
      intros R D D' d is h wf.
      unfold rel_matrix_interpretation in h.
      destruct Domain_naturals; simpl in h; try discr.
      case_eq (matrix_nat arity is (Pos.to_nat d));
        intros p H; rewrite H in h; try discr.
      destruct p as [bge bgt].
      case_eq (ge_R_D R D bge);
        intro H0; rewrite H0 in h; try discr.
      unfold gt_D in h. unfold ge_R_D in H0.
      inversion h. subst D'. clear h. unfold matrix_nat in H.
      revert H.
      case (map_rev (color_interpret_matrix arity (Pos.to_nat d)) is);
        intros l H; try discr.
      case_eq (condition_matrix_nat arity l); intro H2; rewrite H2 in H;
      try discr. inversion H. clear H.
      apply WF_rp_red_mod with (WP:=@WP_Matrix_Nat _ _ l).
      (** Context closed succ *)
      change (context_closed (IR (@AMatrixBasedInt2.I _ Sig _ _
             (@mi_eval_ok _ _ (@TMatrix_Int arity _ coef_sring_N l)))
             (@AMatrixInt2.succ _ _ (@TMatrix_Int _ _ coef_sring_N l)))).
      apply IR_context_closed.
      apply AMatrixInt2.monotone_succ. simpl. intro f.
      apply trsInt_nat_mon. hyp.
      (** Check that rules R is included in succeq *)
      simpl; unfold brule, ds_wr_bsucceq, bsucceq, bool_of_rel; simpl.
      rewrite forallb_forall. intros x Hx. subst bge.
      rewrite andb_eq in H0. destruct H0.
      unfold redpair_matrix_nat_ge in H0.
      rewrite forallb_forall in H0. ded (H0 x Hx).
      destruct x as [t u]. simpl in *.
      destruct (AMatrixBasedInt2.succeq'_dec t u); intros; try discr; auto.
      unfold brule in H1.
      unfold term_ge, term_ord, mint_ge in n.
      eapply bmint_ge_ok in H1. simpl in *.
      unfold mint_ge in H1. simpl in *. try contradiction.
      (** Check that rules D is included in succeq *)
      unfold brule, bsucceq, bool_of_rel; simpl.
      rewrite forallb_forall. intros x Hx. subst bge.
      rewrite andb_eq in H0. destruct H0.
      unfold redpair_matrix_nat_ge in H.
      rewrite forallb_forall in H.
      ded (H x Hx). destruct x as [t u]. simpl in *.
      unfold bsucceq, bool_of_rel.
      destruct AMonAlg2.ma_succeq'_dec; auto.
      unfold brule in H1. simpl in *.
      unfold succeq', AMatrixBasedInt2.succeq',
      term_ge, term_ord, mint_ge in n.
      apply bmint_ge_ok in H1. try contradiction.
      (** Remove all rules D that are in succ. *)
      apply WF_incl with (S:= red_mod (filter (brule (neg bgt)) R)
                                      (filter (brule (neg bgt)) D)).
      unfold inclusion. intros t u H7. redtac. unfold red_mod.
      unfold compose. exists t0. split. simpl in *.
      Focus 2.
      (* red (filter (brule (neg bgt)) D) t0 u *)
      unfold red. exists l0. exists r. exists c.
      exists s. intuition. apply filter_In.
      apply filter_In in lr. intuition.
      unfold brule, neg. unfold brule, neg in H5.
      simpl in *. unfold bsucc, bool_of_rel in H5.
      destruct AMonAlg2.ma_succ'_dec in H5; try discr.
      simpl in *. unfold AMatrixInt2.term_gt, AMatrixBasedInt2.term_gt,
                  term_ord in n; simpl in *; auto.
      unfold AMatrixInt2.mint_gt in n.
      rewrite <- AMatrixInt2.bmint_gt_ok in n.
      apply eq_true_not_negb in n.
      subst bgt. apply n.
    (* red (filter (brule (neg bgt)) R #) t t0 *)
    (* FIXME: fixe the condition in the boolen function. *)
    (* TODO *)
    Admitted.

    (*************************************************************************)
    (** Correctness proof of termination relation [red_mod R D] of
    reduction pair interpretation. *)

    Lemma rel_redPair_interpretation_ok : forall (R D D': arules) t is,
      rel_redPair_interpretation R D t is = Ok D' ->
      WF (red_mod R D') -> WF (red_mod R D).

    Proof.
      intros R D D' t is h wf. destruct t; simpl in h; try discr.
      (** Polynomial interpretation over natural numbers and rational
          numbers. *)
      apply rel_polynomial_interpretation_ok with (D':=D')(is:=is)(d:=d).
      apply h. apply wf.
      (** Matrix interpretation over natural numbers. *)
      destruct d; simpl in h; try discr.
      apply rel_matrix_interpretation_nat_ok with (D':=D')(d:=d0)(is:=is).
      apply h. apply wf.
      (* REMARK: There is no arctic domain for relative termination. *)
    Qed.

    (***********************************************************************)
    (** Relative termination of ordering constrainst proof with
     reduction pair interpretation. Ordering constrainst proof with
     reduction pair interpretation of dependency pair
     transformation. Currently support interpretation only. *)

    Variable rpo_n: nat.

    Definition rel_orderingConstraintProof_redPair (R D:arules) rp
    : error_monad.result arules :=
      match rp with
        | RedPair_interpretation t is    => rel_redPair_interpretation R D t is
        | RedPair_pathOrder sp oaf       => (*pathOrder rpo_n R sp oaf (* TODO *)*)
          Ko _ (Todo Todo1)
        | RedPair_knuthBendixOrder _ _ _ => Ko _ (Todo TRedPair_knuthBendixOrder)
        | RedPair_scnp _ _ _             => Ko _ (Todo TRedPair_scnp)
      end.

    Definition rel_trsTerminationProof_ruleRemoval (R D: arules) ocp :=
      match ocp with
        | OrderingConstraintProof_redPair rp              =>
          rel_orderingConstraintProof_redPair R D rp
        | OrderingConstraintProof_satisfiableAssumption _ =>
          Ko _ (Todo TOrderingConstraintProof_satisfiableAssumption)
      end.

End Top.

(***********************************************************************)
(** Check that [R] is a trivial proof by stating the set of rules
    [R] is empty valid termination proof for [red R]. *)

Definition relTerminationProof_rIsEmpty a (D : arules a) :=
  if   is_empty D
  then OK
  else Ko _ (Error ErNotEmptyrIsEmpty).

Lemma relTerminationProof_rIsEmpty_ok : forall a (R D: arules a),
  relTerminationProof_rIsEmpty D = OK -> WF (red_mod R D).

Proof.
  intros a R D. unfold relTerminationProof_rIsEmpty.
  destruct D; simpl; intro.
  apply WF_red_mod_empty. discr.
Qed.

(***********************************************************************)
(** Check that [p] is a valid termination proof for [red_mod R D].
     - [rIsEmpty] [sIsEmpty]: state that the relative termination is
       terminating since it has no rules.
     - [ruleRemoval]: use a reduction pair where both the weak and the
     strict ordering are monotone. Delete all strictly decreasing
     rules. The remaining rules have to be given. If the ordering
     constraint proof is only an assumption, the
     orderingConstraints-element becomes mandatory.
     - [stringReversal]: reverse the strings in both R and S, i.e., replace
      f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x).  Note that the
      variable in a reversed rule should be same as the variable in the
      original rule.*)

Section S.

  Require Import AUnary AReverse.

  Fixpoint relTerminationProof a (R D: arules a) p : result unit :=
    match p with
      | RelativeTerminationProof_rIsEmpty
      | RelativeTerminationProof_sIsEmpty _                       =>
        relTerminationProof_rIsEmpty D
      | RelativeTerminationProof_ruleRemoval (Some _) _ _ _ _     =>
        Ko _  (Todo TTrsTerminationProof_ruleRemoval)
      | RelativeTerminationProof_ruleRemoval None ocp rs trs p =>
        Match rel_trsTerminationProof_ruleRemoval R D ocp With D' ===>
              relTerminationProof R D' p
      | RelativeTerminationProof_semlab _ _ _ _                   =>
        Ko _ (Todo TTrsTerminationProof_semlab)
      | RelativeTerminationProof_unlab _ _ _                      =>
        Ko _ (Todo TTrsTerminationProof_unlab)
      | RelativeTerminationProof_stringReversal rs rs2 dp         =>
        Ko _ (Todo TTrsTerminationProof_stringReversal)
        (*if   brules_preserve_vars R &&
           brules_preserve_vars D &&
           @bis_unary (Sig a) (symbol_in_rules rs)
        then relTerminationProof (reverse_trs R) (reverse_trs D) dp
        else Ko _ (Todo TTrsTerminationProof_stringReversal)*)
      | RelativeTerminationProof_relativeTerminationAssumption _ =>
        Ko _ (Todo TTrsTerminationProof_terminationAssumption)
      | _  => Ko _ (Todo Todo1)
    end.

    (***********************************************************************)
    (** Structure proof of relation TRS:
       1. relation TRS is empty.
       2. Rule removal.  *)

  Variable nat_of_string : string -> nat.

  Lemma rel_TerminationProof_ok : forall a R D t i,
    sys_of_input a nat_of_string i = Ok (Red_mod R D) ->
    relTerminationProof R D t      = OK -> WF (red_mod R D).

  Proof.
    intros a R D t i H Hs. revert R D H Hs. intros R D Hs.
    clear Hs i. revert t R D.
    induction t; intros R D Hm; simpl in Hm; try discr.
    (** Correctness proof when termination proof is empty. *)
    apply relTerminationProof_rIsEmpty_ok. apply Hm.
    apply relTerminationProof_rIsEmpty_ok. apply Hm.
    (** Correctness proof of relative termination proof in the case of
       rule removal. *)
    destruct o; try discr.
    unfold rel_trsTerminationProof_ruleRemoval in Hm.
    destruct o0; try discr.
    unfold rel_orderingConstraintProof_redPair in Hm.
    destruct r; try discr. revert Hm.
    case_eq (rel_redPair_interpretation R D t2 l); intros l0 H Hm; try discr.
    eapply rel_redPair_interpretation_ok. apply H.
    apply IHt. apply Hm.
  Qed.

  (* TODO
      (** Correctness proof of string reverse. *)
      case_eq (brules_preserve_vars R && brules_preserve_vars D &&
      bis_unary (Sig a) (symbol_in_rules t)); intros H; rewrite H in
      Hm; try discr.  do 2 rewrite andb_eq in H. do 2 destruct H.
      apply WF_red_mod_rev_eq.
      (** Proof that [is_unary] is true. *)
      rewrite <- bis_unary_ok. apply H0.
      (** Proof that [Fs_ok] *)
      Focus 2.
      (** Proof that rule_preserve_vars in D. *)
      rewrite <- brules_preserve_vars_ok. apply H1.
      Focus 2.
      (** Proof that rule_preserve_vars in R. *)
      rewrite <- brules_preserve_vars_ok. apply H.
      Focus 2.
     (* TODO *)
     (* Proof [red_mod (reverse_trs R) (reverse_trs D)] is well-founded *)
     *)

  (***********************************************************************)
  (* TODO: relative non termination Loop *)

  (***********************************************************************)
  (** ** Check that [R] is a violation of variable condition for
    [red_mod R D] *)

  Definition relativeNonTerminationProof_variableConditionViolated a
    (R D: arules a) :=
    if   brules_preserve_vars D
    then Ko _ (Error ErNotVariableConditionViolated)
    else OK.

  Lemma relativeNonTerminationProof_variableConditionViolated_ok: forall a
    (R D: arules a),
    relativeNonTerminationProof_variableConditionViolated R D = OK ->
    EIS (red_mod R D).

  Proof.
    intros a R D Hm.
    unfold relativeNonTerminationProof_variableConditionViolated in Hm.
    case_eq (brules_preserve_vars D); intros H; rewrite H in Hm; try discr.
    apply var_cond_mod.
    rewrite <- brules_preserve_vars_ok.
    rewrite <- false_not_true.
    apply H.
  Qed.

  (***********************************************************************)
  (** ** Check that [p] is a valid non-termination proof for [red_mod
       R D]. Checking that there is a loop in a TRS. *)

  Require Import AModLoop List.

  Definition relativeNonTerminationProof_loop a (R D: arules a)
    (lo: cpf.loop) : result unit :=
    let '((t, ls), _, c) := lo in
    Match color_term a nat_of_string t With t ===>
          (* FIXME: (ls: nil) == list (list rewriteSequence) *)
    Match color_list_mod_data nat_of_string a (ls::nil) With mds ===>
    Match color_rewriteSteps nat_of_string  a  ls       With ds ===>
    let pos := color_position_of_context c in
    if   is_mod_loop R D t mds ds pos
    then OK
    else Ko _ (Error ErrelativeNonTerminationProof_loop).

  Lemma relativeNonTerminationProof_loop_ok: forall a (R D : arules a) l,
    relativeNonTerminationProof_loop R D l = OK -> EIS (red_mod R D).

  Proof.
    intros a R D l Hm.
    unfold relativeNonTerminationProof_loop in Hm.
    destruct l; simpl; try discr.
    destruct p; simpl; try discr.
    destruct r; simpl; try discr.
    case_eq (color_term a nat_of_string t);
      intros t1 H1; rewrite H1 in Hm; try discr.
    case_eq (color_rewriteSteps nat_of_string a l);
      intros ds H2; rewrite H2 in Hm; try discr.
    case_eq (color_list_mod_data nat_of_string a (l :: Datatypes.nil));
      intros mds H3; rewrite H3 in Hm; try discr.
    case_eq (is_mod_loop R D t1 mds ds (color_position_of_context c));
      intros H4; rewrite H4 in Hm; try discr.
    set (p := color_position_of_context c).
    apply is_mod_loop_correct with (t:=t1)(mds:=mds)(ds:=ds)(p:=p).
    apply H4.
    case_eq (color_list_mod_data nat_of_string a (l::Datatypes.nil));
      intros l0 H3; rewrite H3 in Hm; try discr.
  Qed.

  (***********************************************************************)
  (** ** Check that [p] is a valid termination proof for [red_mod R D]

       [variableConditionViolated]: There is a rule where the lhs is a
       variable, or the rhs contains variables not occuring in the lhs.

       [loop]: a loop is given by a (non-empty) rewrite-sequence t0 ->+
       tn where additional tn = C[t0 sigma]. *)

  Definition relativeNonterminationProof a (R D: arules a) p : result unit :=
    match p with
      | RelativeNonterminationProof_loop lo                   =>
        relativeNonTerminationProof_loop R D lo
      | RelativeNonterminationProof_trsNonterminationProof _  =>
        Ko _ (Todo TRelativeNonterminationProof_trsNonterminationProof)
      | RelativeNonterminationProof_variableConditionViolated =>
        relativeNonTerminationProof_variableConditionViolated R D
      | RelativeNonterminationProof_ruleRemoval _ _ _          =>
        Ko _ (Todo TRelativeNonterminationProof_ruleRemoval)
      | RelativeNonterminationProof_nonterminationAssumption _ =>
        Ko _ (Todo TRelativeNonterminationProof_nonterminationAssumption)
    end.

End S.

author: fblanqui

repo: rainbow

save_path: github-repos/coq/fblanqui-rainbow


text:
Load LFindLoad.
From lfind Require Import LFind.
Require Import Arith.

                    From adtind Require Import goal82.

 Require Import Extraction.
 Extract Inductive nat => nat [ "(O)" "S" ].
 Extract Inductive list => list [ "Nil" "Cons" ].
Definition lfind_example_1  := ( Cons (Succ (Succ Zero)) (Cons (Succ (Succ Zero)) Nil)).
Definition lfind_example_2  := ( Cons (Succ (Succ (Succ Zero))) Nil).
Definition lfind_example_3  := ( Cons (Succ (Succ Zero))         (Cons (Succ Zero) (Cons (Succ (Succ Zero)) Nil))).
Definition lfind_example_4  := ( Cons (Succ Zero) Nil).
Definition lfind_example_5  := ( Cons (Succ Zero) (Cons Zero Nil)).
Definition lfind_example_6  := ( Cons Zero Nil).
Definition lfind_example_7  := ( Cons Zero (Cons Zero Nil)).
Definition lfind_example_8  := ( Nil).

                    Extraction "/home/yousef/lemmafinder/benchmark/_lfind_clam_lf_goal82_theorem0_71_qreva_rev/lfind_extraction.ml" lfind_example_1 lfind_example_2 lfind_example_3 lfind_example_4 lfind_example_5 lfind_example_6 lfind_example_7 lfind_example_8 .

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
From Undecidability.L.Tactics Require Import LTactics.
From Undecidability.L.Datatypes Require Import LNat Lists LTerm LOptions LUnit.

From Undecidability.L.Complexity.LinDecode Require Export LTD_def LTDbool LTDlist LTDnat.

From Undecidability.L Require Import Functions.Decoding.

#[export]
Instance linDec_unit : linTimeDecodable unit.
Proof.
  evar (c : nat). exists c.
  unfold decode, decode_unit. cbn. extract.
  solverec. [c]: exact 5. all: unfold c; lia.
Qed.

#[export]
Instance linDec_term : linTimeDecodable term.
Proof.
  evar (c:nat). exists c.
  unfold decode,decode_term;cbn. extract.
  recRel_prettify2;cbn[size];ring_simplify.
  [c]:exact (max (c__linDec nat) 10).
  all:unfold c;try nia.
Qed.

#[export]
Instance linDec_prod X Y `{_ : linTimeDecodable X} `{_:linTimeDecodable Y} : linTimeDecodable (X * Y).
Proof.
  evar (c : nat). exists c.
  unfold decode, decode_prod, prod_decode; cbn.
  extract. recRel_prettify2; cbn [size]; ring_simplify.
  [c]: exact (max (max (c__linDec X) (c__linDec Y)) 14). all: unfold c; try nia.
Qed.

#[export]
Instance linDec_sum X Y `{_ : linTimeDecodable X} `{_:linTimeDecodable Y} : linTimeDecodable (X + Y).
Proof.
  evar (c : nat). exists c.
  unfold decode, decode_sum, sum_decode; cbn.
  extract. recRel_prettify2; cbn [size]; ring_simplify.
  [c]: exact (max (max (c__linDec X) (c__linDec Y)) 14). all: unfold c; try nia.
Qed.

author: uds-psl

repo: coq-library-complexity


(*** Barrett Reduction *)
(** This file implements Barrett Reduction on [Z].  We follow Wikipedia. *)
Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Tactics.BreakMatch.

Local Open Scope Z_scope.

Section barrett.
  Context (n a : Z)
          (n_reasonable : n <> 0).
  (** Quoting Wikipedia <https://en.wikipedia.org/wiki/Barrett_reduction>: *)
  (** In modular arithmetic, Barrett reduction is a reduction
      algorithm introduced in 1986 by P.D. Barrett. A naive way of
      computing *)
  (** [c = a mod n] *)
  (** would be to use a fast division algorithm. Barrett reduction is
      an algorithm designed to optimize this operation assuming [n] is
      constant, and [a < n²], replacing divisions by
      multiplications. *)

  (** * General idea *)
  Section general_idea.
    (** Let [m = 1 / n] be the inverse of [n] as a floating point
        number. Then *)
    (** [a mod n = a - ⌊a m⌋ n] *)
    (** where [⌊ x ⌋] denotes the floor function. The result is exact,
        as long as [m] is computed with sufficient accuracy. *)

    (* [/] is [Z.div], which means truncated division *)
    Local Notation "⌊am⌋" := (a / n) (only parsing).

    Theorem naive_barrett_reduction_correct
      : a mod n = a - ⌊am⌋ * n.
    Proof using n_reasonable.
      apply Zmod_eq_full; assumption.
    Qed.
  End general_idea.

  (** * Barrett algorithm *)
  Section barrett_algorithm.
    (** Barrett algorithm is a fixed-point analog which expresses
        everything in terms of integers. Let [k] be the smallest
        integer such that [2ᵏ > n]. Think of [n] as representing the
        fixed-point number [n 2⁻ᵏ]. We precompute [m] such that [m =
        ⌊4ᵏ / n⌋]. Then [m] represents the fixed-point number
        [m 2⁻ᵏ ≈ (n 2⁻ᵏ)⁻¹]. *)
    (** N.B. We don't need [k] to be the smallest such integer. *)
    Context (k : Z)
            (k_good : n < 2 ^ k)
            (m : Z)
            (m_good : m = 4^k / n). (* [/] is [Z.div], which is truncated *)
    (** Wikipedia neglects to mention non-negativity, but we need it.
        It might be possible to do with a relaxed assumption, such as
        the sign of [a] and the sign of [n] being the same; but I
        figured it wasn't worth it. *)
    Context (n_pos : 0 < n) (* or just [0 <= n], since we have [n <> 0] above *)
            (a_nonneg : 0 <= a).

    Lemma k_nonnegative : 0 <= k.
    Proof using Type*.
      destruct (Z_lt_le_dec k 0); try assumption.
      rewrite !Z.pow_neg_r in * by lia; lia.
    Qed.

    (** Now *)
    Let q := (m * a) / 4^k.
    Let r := a - q * n.
    (** Because of the floor function (in Coq, because [/] means
        truncated division), [q] is an integer and [r ≡ a mod n]. *)
    Theorem barrett_reduction_equivalent
      : r mod n = a mod n.
    Proof using m_good.
      subst r q m.
      rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption.
      reflexivity.
    Qed.

    Lemma qn_small
      : q * n <= a.
    Proof using a_nonneg k_good m_good n_pos n_reasonable.
      pose proof k_nonnegative; subst q r m.
      assert (0 <= 2^(k-1)) by zero_bounds.
      Z.simplify_fractions_le.
    Qed.

    (** Also, if [a < n²] then [r < 2n]. *)
    (** N.B. It turns out that it is sufficient to assume [a < 4ᵏ]. *)
    Context (a_small : a < 4^k).
    Lemma q_nice : { b : bool | q = a / n + if b then -1 else 0 }.
    Proof using a_nonneg a_small k_good m_good n_pos n_reasonable.
      assert (0 <= (4 ^ k * a / n) mod 4 ^ k < 4 ^ k) by auto with zarith lia.
      assert (0 <= a * (4 ^ k mod n) / n < 4 ^ k) by (auto with zero_bounds zarith lia).
      subst q r m.
      rewrite (Z.div_mul_diff_exact''' (4^k) n a) by lia.
      rewrite (Z_div_mod_eq (4^k * _ / n) (4^k)) by lia.
      autorewrite with push_Zmul push_Zopp zsimplify zstrip_div.
      eexists; reflexivity.
    Qed.

    Lemma r_small : r < 2 * n.
    Proof using a_nonneg a_small k_good m_good n_pos n_reasonable q.
      Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div.
      assert (a mod n < n) by auto with zarith lia.
      unfold r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m.
      autorewrite with push_Zmul zsimplify zstrip_div.
      break_match; auto with lia.
    Qed.

    (** In that case, we have *)
    Theorem barrett_reduction_small
      : a mod n = if r <? n
                  then r
                  else r - n.
    Proof using a_nonneg a_small k_good m_good n_pos n_reasonable q.
      pose proof r_small. pose proof qn_small.
      destruct (r <? n) eqn:rlt; Z.ltb_to_lt.
      { symmetry; apply (Zmod_unique a n q); subst r; lia. }
      { symmetry; apply (Zmod_unique a n (q + 1)); subst r; lia. }
    Qed.
  End barrett_algorithm.
End barrett.


text:
Inductive Tree : Set :=
|children : list Tree -> Tree.

(*Wrong!*)

Fixpoint length(t:Tree) : nat :=
match t with
|children l => S (length_forest l)
end
with length_forest(f:list Tree) : nat :=
match f with
|nil => 0
|cons t ts => (length t) + (length_forest ts)
end.

(*
Recursive definition of length_forest is ill-formed.
In environment
length : Tree -> nat
length_forest : list Tree -> nat
f : list Tree
t : Tree
ts : list Tree
Recursive call to length has principal argument equal to
"t" instead of "ts".
Recursive definition is:
"fun f : list Tree =>
 match f with
 | nil => 0
 | (t :: ts)%list => length t + length_forest ts
 end".
*)

(* Right! *)

Fixpoint length(t:Tree) : nat :=
  Tree_rect (fun _ : Tree => nat)
    (fun l : list Tree =>
     list_rec (fun _ : list Tree => nat) 1
       (fun (a : Tree) (_ : list Tree) (IHl : nat) => length a + IHl) l) t.

author: bowtochris

repo: CoqStuff

save_path: github-repos/coq/bowtochris-CoqStuff


text:
(*
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 * http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 *)

Require Import String.
Require Import List.
Require Import ZArith.
Require Import Compare_dec.
Require Import Utils.
Require Import Types.
Require Import DataModel.
Require Import ForeignData.
Require Import ForeignOperators.
Require Import ForeignDataTyping.
Require Import Operators.
Require Import TData.
Require Import TUtil.
Require Import GroupBy.

Section TGroupBy.

  Context {fdata:foreign_data}.
  Context {ftype:foreign_type}.
  Context {fdtyping:foreign_data_typing}.
  Context {m:brand_model}.

  Import ListNotations.

  Definition GroupBy_type
             (g : string)
             (sl : list string)
             (k : record_kind)
             (τl : list (string * rtype))
             (pf : is_list_sorted ODT_lt_dec (domain τl) = true)
    : rtype
    := Coll
         (Rec Closed
              (rec_concat_sort
                 (rproject τl sl) [(g, Coll (Rec k τl pf))]) rec_sort_pf).

  Lemma typed_group_to_partitions_yields_typed_data
        {key:data} {values:list data} {τkeys pf τvalues} :
    key ▹ Rec Closed τkeys pf ->
    Forall (fun v => v ▹ τvalues) values ->
    forall g,
    exists d' : data,
      group_to_partitions g (key,values) = Some d'
      /\  d' ▹ Rec Closed (rec_concat_sort τkeys [(g,Coll τvalues)]) rec_sort_pf.
  Proof.
    Opaque rec_sort.
    intros.
    unfold group_to_partitions; simpl.
    dtype_inverter.
    eexists; split; [reflexivity | ].
    invcs H.
    rtype_equalizer; subst.
    intuition; subst.
    eapply dtrec; try reflexivity.
    - generalize (drec_sort_sorted  (rl ++ [(g,Coll τvalues)])); simpl; trivial.
    - apply rec_sort_Forall2; simpl.
      + repeat rewrite domain_app; f_equal.
        apply sorted_forall_same_domain; trivial.
      + apply Forall2_app; trivial; simpl.
        constructor; simpl; trivial.
        split; trivial.
        constructor; trivial.
        Transparent rec_sort.
  Qed.

  Lemma typed_to_partitions_yields_typed_data
        {g:string}
        (l:list (data*list data))
        {τkeys pf τvalues}  :
    Forall (fun kv =>
              (fst kv) ▹ Rec Closed τkeys pf /\
              Forall (fun v => v ▹ τvalues) (snd kv)) l ->
    exists dl' : list data,
      to_partitions g l = Some dl'
      /\ Forall (fun d' => d' ▹ Rec Closed (rec_concat_sort τkeys [(g,Coll τvalues)]) rec_sort_pf) dl'.
  Proof.
    unfold to_partitions; intros F.
    apply lift_map_Forall_exists_and.
    revert F.
    apply Forall_impl; intros.
    destruct a; destruct H as [typ F]; simpl in *.
    apply (typed_group_to_partitions_yields_typed_data typ F).
  Qed.

  Lemma typed_group_of_key_yields_typed_data eval_key k l τ :
    Forall (fun d => d ▹ τ) l ->
    Forall (fun d => exists y, eval_key d = Some y) l ->
    exists dl' : list data,
      group_of_key eval_key k l = Some dl'
      /\ Forall (fun d' => d' ▹ τ) dl'.
  Proof.
    intros.
    unfold group_of_key.
    destruct (lift_filter_Forall_exists
                (fun d : data => key_is_eq_r eval_key d k) l)
      as [dl' [eqq subl]].
    - revert H0. apply Forall_impl; intros ? [? eqq].
      unfold key_is_eq_r.
      rewrite eqq; simpl.
      match_destr; eauto.
    - exists dl'; split; trivial.
      rewrite subl; trivial.
  Qed.

  Lemma typed_group_by_nested_eval_yields_typed_data eval_key l τ τ' :
    Forall (fun d => d ▹ τ) l ->
    Forall (fun d => exists y, eval_key d = Some y /\ y ▹ τ') l ->
    exists dl' : list (data*list data),
      group_by_nested_eval eval_key l = Some dl'
      /\ Forall (fun d'dl' => (fst d'dl') ▹ τ' /\ Forall (fun d => d▹ τ) (snd d'dl')) dl'.
  Proof.
    intros F1 F2.
    unfold group_by_nested_eval.
    destruct (lift_map_Forall_exists_and (fun d : data => eval_key d) l F2)
      as [l1 [eqq Pl1]].
    rewrite eqq; simpl.
    apply lift_map_Forall_exists_and.
    apply bdistinct_Forall.
    revert Pl1.
    apply Forall_impl; intros.
    assert (F2': Forall (fun d : data => exists y : data, eval_key d = Some y) l).
    { revert F2; apply Forall_impl; firstorder. }
    destruct (typed_group_of_key_yields_typed_data _ a _ _ F1 F2')
      as [g [eqq3 F3]].
    rewrite eqq3; simpl.
    eauto.
  Qed.

  Lemma typed_group_by_nested_eval_keys_partition_yields_typed_data g eval_key l τ τkeys pf :
    Forall (fun d => d ▹ τ) l ->
    Forall (fun d => exists y, eval_key d = Some y /\ y ▹ Rec Closed τkeys pf) l ->
    exists dl' : list data,
      group_by_nested_eval_keys_partition g eval_key l = Some dl'
      /\ Forall (fun d' => d' ▹ Rec Closed (rec_concat_sort τkeys [(g,Coll τ)]) rec_sort_pf) dl'.
  Proof.
    intros F1 F2.
    unfold group_by_nested_eval_keys_partition.
    destruct (typed_group_by_nested_eval_yields_typed_data _ _ _ _ F1 F2)
      as [? [eqq3 F3]].
    rewrite eqq3; simpl.
    eapply typed_to_partitions_yields_typed_data; eauto.
  Qed.

  Lemma typed_group_by_nested_eval_table_yields_typed_data {d k τl pf} :
    dcoll d ▹ Coll (Rec k τl pf) ->
    forall g sl,
      sublist sl (domain τl) ->
    exists d' : data,
      lift dcoll (group_by_nested_eval_table g sl d) = Some d'
      /\ d' ▹ GroupBy_type g sl k τl pf .
  Proof.
    unfold GroupBy_type.
    intros.
    apply Col_inv in H.
    unfold group_by_nested_eval_table.
    assert (projsort: is_list_sorted ODT_lt_dec (domain (rproject τl sl)) = true).
    { apply (is_list_sorted_sublist pf).
      apply sublist_domain.
      apply sublist_rproject.
    }
    generalize (typed_group_by_nested_eval_keys_partition_yields_typed_data
                  g
                  (fun d =>
                     match d with
                     | drec r => Some (drec (rproject r sl))
                     | _ => None
                     end) d (Rec k τl pf) (rproject τl sl) projsort); intros HH.
    cut_to HH; trivial.
    - destruct HH as [? [eqq1 F1]].
      rewrite eqq1; simpl; eexists; split; try reflexivity.
      constructor; trivial.
    - clear HH.
      revert H; apply Forall_impl; intros.
      dtype_inverter.
      eexists; split; try reflexivity.
      apply dtrec_full.
      invcs H; rtype_equalizer; subst; trivial.
      apply (rproject_well_typed _ rl); trivial.
  Qed.

End TGroupBy.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert


text:
Set Implicit Arguments.
Unset Strict Implicit.

Require Import basics.
Require Import enat.
Require Import allen.

Section signal.

Ltac G x := generalize x.

Ltac BAD := intros BAD; inversion BAD.

Ltac INC_CMP CV1 CV2 :=
  intros I J (LL,RR);
  apply (inc_allen_by_comp2 (CV1 _ _ LL) (CV2 _ _ RR)).

Ltac RINC_CMP CV1 CV2 :=
  intros I J (LL,RR);
  apply (inc_allen_by_comp2 (CV1 _ _ LL) (CV2 _ _ RR)).

(*
 * Signals
 *)
Definition sig := nat -> Prop.

(*
 * EQ_SIG
 *)
Definition eq_sig (p q:sig) := forall (t:nat), (p t)<->(q t).

Lemma eq_sig_sym (p q:sig) : (eq_sig p q) <-> (eq_sig q p).
split;intros EQ;intros t;rewrite (EQ t);tauto.
Qed.

(*
 * NOT
 *)
Definition not_sig (p:sig) : sig := fun t => ~(p t).

Lemma not_sig_def (p:sig) (t:nat) : ((not_sig p) t) = ~(p t).
auto.
Qed.

Lemma not_not_sig_def (p:sig) (t:nat) : (~((not_sig p) t)) <-> (p t).
rewrite not_sig_def.
apply not_not.
Qed.

Lemma eq_sig_not_not (p:sig) : (eq_sig (not_sig (not_sig p)) p).
intros t.
repeat rewrite not_sig_def.
rewrite not_not.
tauto.
Qed.

(*
 * On/Off
 *)
Definition on (I:allen) (p:sig) := (forall t, (in_allen t I) -> (p t)).

Definition off (I:allen) (p:sig) := (forall t, (in_allen t I) -> ~(p t)).

Lemma on_left (p:sig) (I:allen) : (on I p) -> (p (left I)).
intros IInp.
apply (IInp _ (in_allen_left I)).
Qed.

Lemma inc_allen_on (p:sig) (I J:allen) :
 (inc_allen I J) ->
 (on J p) ->
 (on I p).
intros INC JInp t tInI.
apply (JInp t (INC _ tInI)).
Qed.

(*
 * in_sig
 *)
Definition in_sig  (I:allen) (p:sig) : Prop :=
    (match (left I) with 0 => True | (S t) => ~(p t) end)
 /\ (match (right I) with Inf => True | Fix t => ~(p t) end)
 /\ (on I p).

Lemma eq_allen_in_sig p I J :
 (eq_allen I J) ->
 (in_sig I p) ->
 (in_sig J p).
intros (EQL,EQR) (LEFT,(RIGHT,SLICE)).
split;[|split];
unfold in_sig.
- rewrite <- EQL; auto.
- rewrite <- EQR; auto.
- intros t tInJ.
  apply SLICE.
  apply inc_allen_refl with (I:=J) (J:=I); auto.
  apply eq_allen_sym; split; auto.
Qed.

(* Basic borders *)
Lemma previous_left_out (p:sig) (I:allen) (pl:nat) :
 (in_sig I p) ->
 (left I) = (S pl) ->
 ~(p pl).
intros (OK,_) LI.
rewrite LI in OK; auto.
Qed.

Lemma bounded_right_out p I r :
 (in_sig I p) ->
 (right I)=(Fix r) ->
 ~(p r).
intros (_,(OK,_)) RI.
rewrite RI in OK; auto.
Qed.

Lemma in_sig_slice I p :
 (in_sig I p) ->
 (on I p).
intros (_,(_,OK)); auto.
Qed.

Lemma in_left (p:sig) (I:allen) : (in_sig I p) -> (p (left I)).
intros IInp.
apply (in_sig_slice IInp (in_allen_left I)).
Qed.

Lemma previous_right_in (I:allen) (p:sig) (r:nat) :
 (in_sig I p) ->
 (right I) = (Fix (S r)) ->
 (p r).
intros IInp RI.
apply (in_sig_slice IInp).
split.
- G (wf I).
  rewrite RI; simpl; auto with arith.
- rewrite RI; simpl; auto.
Qed.

(* safe *)
Definition safe_allen_relation (R:(allen->allen->Prop)) := forall I1 I2 J1 J2,
 (eq_allen I1 I2) ->
 (eq_allen J1 J2) ->
 (R I1 J1) ->
 (R I2 J2).

Lemma safe_allen_fun_extend (R:(allen -> allen -> Prop)) (q:sig) :
 (safe_allen_relation R) ->
 (safe_allen_fun (fun I => (exists J, (in_sig J q) /\ (R I J)))).
intros SR I1 I2 EQ (J,(Jq,R1)).
exists J. split;[auto|].
apply (SR _ _ _ _ EQ (eq_allen_refl J) R1).
Qed.

(*
 * ORDERS
 * inc_sig p q : (p t) -> (q t)
 * inc_sig_allen p q : I\in p -> I\in q
 *)

Definition inc_sig (p q:sig) := forall (t:nat),
  (p t) -> (q t).

Lemma inc_sig_trans (p q r:sig) : (inc_sig p q) -> (inc_sig q r) -> (inc_sig p r).
intros PQ QR t Pt.
apply (QR t (PQ t Pt)).
Qed.

Definition inc_sig_allen (p q:sig) := forall (I:allen),
 (in_sig I p) -> (in_sig I q).

Lemma in_sig_fixl_gt0 I : (ilt (Fix 0) (right I)).
generalize (wf I).
case (right I) as [t|]; simpl; auto.
intros LT.
apply (lt_0lt LT).
Qed.

(*
 * TON
 *)
Definition ton (t:nat) (I:allen) (p:sig) := (in_allen t I) /\ (on I p).

Lemma ton_def (t:nat) (I:allen) (p:sig) :
 (in_allen t I) -> (on I p) -> (ton t I p).
split; auto.
Qed.

Lemma ton_allen  (t:nat) (I:allen) (p:sig) : (ton t I p) -> (in_allen t I).
intros (OK,_); auto.
Qed.

Lemma ton_sig  (t:nat) (I:allen) (p:sig) : (ton t I p) -> (on I p).
intros (_,OK); auto.
Qed.

Lemma ton_p (t:nat) (I:allen) (p:sig) : (ton t I p) -> (p t).
intros (tI,IN).
apply (IN _ tI).
Qed.

(*
 * TAS
 *)
Definition tas (t:nat) (I:allen) (p:sig) := (in_allen t I) /\ (in_sig I p).

Lemma tas_ton (t:nat) (I:allen) (p:sig) : (tas t I p) -> (ton t I p).
intros (tI,(_,(_,OK))). split; auto.
Qed.

Lemma tas_def (t:nat) (I:allen) (p:sig) :
 (in_allen t I) -> (in_sig I p) -> (tas t I p).
split; auto.
Qed.

Lemma tas_allen  (t:nat) (I:allen) (p:sig) : (tas t I p) -> (in_allen t I).
intros (OK,_); auto.
Qed.

Lemma tas_sig  (t:nat) (I:allen) (p:sig) : (tas t I p) -> (in_sig I p).
intros (_,OK); auto.
Qed.

Lemma tas_on (p:sig) (I:allen) (t:nat) : (tas t I p) -> (on I p).
intros (_,(_,(_,OK))); auto.
Qed.

Lemma tas_p (t:nat) (I:allen) (p:sig) : (tas t I p) -> (p t).
intros (tI,Ip).
apply (in_sig_slice Ip tI).
Qed.

Lemma in_sig_tas_left (p:sig) (I:allen) : (in_sig I p) -> (tas (left I) I p).
intros Ip. apply (tas_def (in_allen_left I) Ip).
Qed.

Lemma tas_left (p:sig) (I:allen) (t:nat) : (tas t I p) -> (tas (left I) I p).
intros tIp.
apply (in_sig_tas_left (tas_sig tIp)).
Qed.

Lemma tas_mov (p:sig) (I:allen) (t t':nat) :
 (tas t I p) ->
 (in_allen t' I) ->
 (tas t' I p).
intros tIp t'I.
apply (tas_def t'I (tas_sig tIp)).
Qed.

Lemma inc_in_on (p q:sig) (I:allen) :
 (inc_sig p q) ->
 (in_sig I p) ->
 (on I q).
intros INC Ip t tI.
apply (INC t (tas_p (tas_def tI Ip))).
Qed.

(* On successive points *)

Lemma in_allen_in_sig__on_succ (p:sig) (I:allen) (t:nat) :
 (tas t I p) ->
 (p (S t)) ->
 (in_allen (S t) I).
intros ((LEFT,RIGHT),IInp) PSt.
split;[auto|].
case_eq (right I); simpl; auto.
intros r RI.
rewrite RI in RIGHT; simpl in RIGHT.
G (nat_compare (S t) r);intros [LE|[EQ|GT]];[auto | | ].
- exfalso.
  G PSt. rewrite EQ.
  apply (bounded_right_out IInp RI).
- exfalso.
  apply (too_small_segment (x:=t)(y:=r)); auto.
Qed.

Lemma in_allen_in_sig__on_prev (p:sig) (I:allen) (t:nat) :
 (tas (S t) I p) ->
 (p t) ->
 (in_allen t I).
intros ((LEFT,RIGHT),IInp) Pt.
split;[|apply (ilt_succ RIGHT)].
case_eq (left I); [auto with arith | intros l LI].
rewrite LI in LEFT.
G (nat_compare (S l) t);intros [LE|[EQ|GT]];[auto with arith| | ].
- rewrite EQ; auto.
- exfalso.
  G (single_segment (le_succ_r LEFT) GT); intros EQ.
  G Pt. rewrite <- EQ.
  apply (previous_left_out IInp LI).
Qed.

Lemma in_allen_in_sig_follow_right (p:sig) (I:allen) (t t':nat) :
 (tas t I p) ->
 (forall x, (t<x) -> (x<=t') -> (p x)) ->
 (ilt (Fix t') (right I)).
intros (tInI,IInp) Slice.
case_eq (right I);simpl;[intros ri RI|auto].
rewrite <- not_not, <- le__not_lt.
intros LE.
cut (p ri);[apply (bounded_right_out IInp RI)|].
apply Slice;[|auto].
G (allen_right tInI). rewrite RI. auto.
Qed.

(* inc_sig *)
Lemma inc_sig_asym (p q:sig) :
 (inc_sig p q) ->
 (inc_sig q p) ->
 (eq_sig p q).
intros PInQ QInP t.
split; [intros Pt; apply (PInQ _ Pt)|intros Qt; apply (QInP _ Qt)].
Qed.

Lemma tas_inc_tas (p q:sig) (I J:allen) (t:nat) :
 (tas t I p) ->
 (in_sig J q) ->
 (inc_allen I J) ->
 (tas t J q).
intros tIp Jq INC.
apply (tas_def (INC _ (tas_allen tIp)) Jq).
Qed.

Lemma tas_by_include (p q:sig) (I J:allen) (t:nat) :
 (tas t I p) ->
 (in_sig J q) ->
 (inc_allen I J) ->
 (tas t J q).
intros (tInI,IInp) JInq INC.
split;[|auto].
apply (in_allen_by_include tInI (inc_allen_left INC) (inc_allen_right INC)).
Qed.

(* inc_allen *)
Lemma not_and_or_not (P Q:Prop) : ~(P /\Q) -> (~P \/ ~Q).
tauto.
Qed.

Lemma not_inc_allen (I J:allen) :
  (not (inc_allen I J)) ->
  (exists t, (in_allen t I) /\ (t<(left J) \/ (ile (right J) (Fix t)))).
intros NINC.
G (not_all_ex_not _ _ NINC). clear NINC. intros (t,NIMP).
exists t.
G (not_imply_and NIMP). clear NIMP. intros (tI,NIN).
split;[auto|].
G (not_and_or_not NIN). clear tI NIN. intros [LT | LE];[left|right].
- rewrite le__not_lt in LT.  tauto.
- rewrite ile__not_ilt. auto.
Qed.

Lemma in_allen_in_sig_slice__inc_allen (p:sig) (I J:allen) (t:nat) :
 (in_allen t I) ->
 (in_allen t J) ->
 (in_sig J p) ->
 (on I p) ->
 (inc_allen I J).
intros tInI tInJ JInp SLIp.
apply left_right_inc_allen.
- (* use tas_tas_not_left_lt *)
  rewrite le__not_lt.
  case_eq (left J); [|intros pl];intros LJ.
  + apply nlt0.
  + G (previous_left_out JInp LJ).
    apply ncontra. intros LI.
    apply SLIp.
    split.
    * apply ltS__le; auto.
    * G (allen_left tInJ); rewrite LJ; intros LE.
      apply (lt_ilt_trans (leS_lt LE) (allen_right tInI)).
- case_eq (right J); [intros r|]; intros RJ.
  + rewrite ile__not_ilt.
    G (bounded_right_out JInp RJ).
    apply ncontra. intros LT.
    apply SLIp.
    split;[|auto].
    apply lt_le.
    G (allen_right tInJ); rewrite RJ; simpl.
    G (allen_left tInI).
    apply le_lt_trans.
  + apply ile_inf.
Qed.

Lemma in_allen_in_sig_slice__inc_allen2 (p:sig) (I J:allen) (t:nat) :
 (in_allen t I) ->
 (tas t J p) ->
 (on I p) ->
 (inc_allen I J).
intros tInI (tInJ,JInq) INC.
apply (in_allen_in_sig_slice__inc_allen tInI tInJ JInq INC).
Qed.

(* inc_sig_allen *)

Lemma inc_sig_allen_refl (p q:sig) :
 (eq_sig p q) ->
 (inc_sig_allen p q).
intros EQ I IInp.
split;[|split].
- case_eq (left I); auto; intros pl LI.
  rewrite <- (EQ pl).
  apply (previous_left_out IInp LI).
- case_eq (right I); auto; intros r RI.
  rewrite <- (EQ r).
  apply (bounded_right_out IInp RI).
- intros t tInI.
  G (in_sig_slice IInp tInI); rewrite <- (EQ t); auto.
Qed.

Lemma eq_sig_tas (p q:sig) (I:allen) (t:nat) :
 (eq_sig p q) ->
 (tas t I p) ->
 (tas t I q).
intros EQ (tInI,IInp).
split;[auto|].
apply (inc_sig_allen_refl EQ IInp).
Qed.

(*
 * finding the allen interval from a time point
 *)

Lemma dec_step (P NP:Prop) : (NP<->~P) -> (P\/NP).
tauto.
Qed.

Lemma not_for__ex_not (T:Type) (x:T) (P:T->Prop) :
 (~(forall x, (P x))) <-> (exists x, ~(P x)).
split.
- apply not_all_ex_not.
- apply ex_not_not_all.
Qed.

Lemma hole_in_left (f:nat->Prop) (t:nat) :
    (forall t', (t'<t) -> ((f t')<->(f t)))
 \/ (exists M, (M<t) /\ ~((f M) <-> (f t))).
apply dec_step.
rewrite not_for__ex_not; auto.
split; intros (x,P); exists x; tauto.
Qed.

Lemma hole_in_right (f:nat->Prop) (t:nat) :
    (forall t', (t<t') -> ((f t')<->(f t)))
 \/ (exists M, (t<M) /\ ~((f M) <-> (f t))).
apply dec_step.
rewrite not_for__ex_not; auto.
split; intros (x,P); exists x; tauto.
Qed.

Lemma sigf_compare (f:nat->Prop) (t1 t2:nat) :
 ((f t1) <-> (f t2)) \/ ((f t1) <-> ~(f t2)).
tauto.
Qed.

Lemma search_left (f:nat->Prop) (t:nat) :
 (   (forall t', t'<t -> ((f t') <-> (f t)))
  \/ (exists m, (m<t)
             /\ ~((f m) <-> (f t))
             /\ (forall t', (m<t'<t -> ((f t') <-> (f t)))) )).
induction t as [|t [SUS|(m,(LT,(NOT,SLICE)))]].
- left; intros t'; BAD.
- G (sigf_compare f t (S t)); intros [EQ|NEQ].
  + left; intros t' LT.
    rewrite <- EQ.
    G (ltSucc LT); intros [LT2|EQ2]; auto.
    rewrite EQ2; tauto.
  + right; exists t; split;[auto|split;[tauto|]].
    intros t' SEG.
    exfalso.
    apply (too_small_segment SEG).
- G (sigf_compare f t (S t)); intros [EQ|NEQ].
  + right; exists m.
    split;[auto with arith|split;[rewrite <-EQ;auto|]].
    intros t' (LT1,LT2).
    rewrite <- EQ.
    G (ltSucc LT2); intros [LT3|EQ3]; auto.
    rewrite EQ3; tauto.
  + right; exists t; split;[auto|split;[tauto|]].
    intros t' SEG.
    exfalso.
    apply (too_small_segment SEG).
Qed.

Lemma try_find_left (f:nat->Prop) (t:nat) :
 (f t) ->
 (   (forall t', t'<t -> (f t'))
  \/ (exists m, (m<t)
            /\ ~(f m)
            /\ (forall t', (m<t'<t -> (f t')))) ).
intros Ft.
G (search_left f t); intros [SUS|(m,(LT,(NOT,SLICE)))].
- left; intros t' LT.
  rewrite (SUS _ LT); auto.
- right.
  exists m; split;[auto|split;[tauto|]].
  intros t' SEG.
  rewrite (SLICE _ SEG); auto.
Qed.

Lemma try_find_left2 (f:nat->Prop) (t:nat) :
 (f t) ->
 (   (forall t', t'<t -> (f t'))
  \/ (exists m, (m<t)
            /\ ~(f m)
            /\ (forall t', m<t' -> t'<=t -> (f t'))) ).
intros Ft.
G (search_left f t); intros [SUS|(m,(LT,(NOT,SLICE)))].
- left; intros t' LT.
  rewrite (SUS _ LT); auto.
- right.
  exists m; split;[auto|split;[tauto|]].
  intros t' SEG.
  rewrite le_fix_def.
  intros [GT|EQ]; [rewrite SLICE|rewrite EQ]; auto.
Qed.

Lemma seg_choice_left_ind (f:nat->Prop) (m:nat) : forall n,
    (forall t, m<t<m+n -> ((f t) <-> (f m)))
 \/ (exists t, m<t<(m+n)
            /\ ~((f t) <-> (f m))
            /\ (forall x, m<x<t -> ((f x) <-> (f m))) ).
induction n as [|n [SL|(t,((LT,GT),(NEQ,SLI)))]].
- left.
  replace (m+0) with m; auto.
  intros t (B1,B2).
  exfalso.
  apply (lt_asym _ _ B1 B2).
- G (sigf_compare f m (m+n)); intros [EQ|DIFF].
  + left.
    intros t (LT,GT).
    G (nat_compare t (m+n)); intros [LT2|[EQ2|GT2]].
    * apply SL.
      split; auto with arith.
    * rewrite EQ2; tauto.
    * exfalso; apply (too_small_segment (x:=(m+n)) (y:=t)).
      replace (S (m+n)) with (m+(S n)); auto.
  + case n as [|n].
    * replace (m+0) with m in DIFF; auto.
      exfalso; tauto.
    * right.
      exists (m+(S n)).
      split; [|tauto].
      split; auto with arith.
      apply lt_add_S.
- right.
  exists t.
  split; [split;[auto|]|auto].
  apply (lt_trans _ _ _ GT).
  auto with arith.
Qed.

Lemma seg_choice_left (f:nat->Prop) (m M:nat) :
  (m < M) ->
    (forall t, m<t<M -> ((f t) <-> (f m)))
 \/ (exists t, m<t<M
            /\ ~((f t) <-> (f m))
            /\ (forall x, m<x<t -> ((f x) <-> (f m))) ).
intros LTS.
G (seg_choice_left_ind f m (M-m)); intros [SLI|(t,((LT,GT),(NEQ,SLE)))].
- replace (m+(M-m)) with M in SLI;[|auto with arith].
  left; auto.
- replace (m+(M-m)) with M in GT;[|auto with arith].
  right; exists t; auto.
Qed.

Lemma search_right (f:nat->Prop) (t:nat) :
    (forall t', t<t' -> ((f t')<->(f t)))
 \/ (exists M, t<M
            /\ ~((f M) <-> (f t))
            /\ (forall t', t<t'<M -> ((f t') <-> (f t))) ).
G (hole_in_right f t); intros [ALL|(H,(LT,HOLE))].
- left; auto.
- right; G (seg_choice_left f LT); intros [SLI|(M,((LTM,GTM),(NOT,SLI)))].
  + exists H; auto.
  + exists M; auto.
Qed.

Lemma try_find_right (f:nat->Prop) (t:nat) :
 (f t) ->
    (forall t', t<t' -> (f t'))
 \/ (exists M, t<M
            /\ ~(f M)
            /\ (forall t', t<t'<M -> (f t')) ).
intros Ft.
G (search_right f t); intros [SUS|(M,(LT,(NOT,SLICE)))].
- left; intros t' LT.
  rewrite (SUS _ LT); auto.
- right.
  exists M; split;[auto|split;[tauto|]].
  intros t' SEG.
  rewrite (SLICE _ SEG); auto.
Qed.

Lemma get_sig (p:sig) (t:nat) : (p t) -> (exists I, (tas t I p)).
intros Pt.
G (try_find_left Pt); intros [SUSL|(m,(LT,(LEFT,SL1)))];
 G (try_find_right Pt); intros [SUSR|(M,(GT,(RIGHT,SL2)))].
- exists (make_allen (m:=0) (M:=Inf) (ilt__inf 0)).
  split;[split;[auto with arith|simpl;auto]|split;[split|split;[split|]]].
  intros t' _.
  G (nat_compare t t'); intros [LE|[EQ|GT]];
    [apply (SUSR _ LE)|rewrite <- EQ|apply (SUSL _ GT)]; auto.
- exists (make_allen (m:=0) (M:=(Fix M)) (lt_0ilt GT)).
  split;[split;[auto with arith|simpl;auto]|split;[split|split;[auto|]]].
  intros t' (_,LT'). simpl in LT'.
  G (nat_compare t t'); intros [LE|[EQ|GT2]];
    [apply SL2|rewrite <- EQ|apply (SUSL _ GT2)]; auto.
- exists (make_allen (m:=(S m)) (M:=Inf) (ilt__inf (S m))).
  split;[split;[auto with arith|simpl;auto]|split;[auto|split;[split|]]].
  intros t' (LE2,_). simpl in LE2.
  G (nat_compare t t'); intros [LE|[EQ|GT2]];
    [apply SUSR|rewrite <- EQ|apply SL1]; auto.
- exists (make_allen (m:=(S m)) (M:=(Fix M)) (lt_iltS_trans LT GT)).
  split;[split;[auto with arith|simpl;auto]|split;[auto|split;[auto|]]].
  intros t' (LE2,LE3). simpl in LE2. simpl in LE3.
  G (nat_compare t t'); intros [LE|[EQ|GT2]];
    [apply SL2|rewrite <- EQ|apply SL1]; auto.
Qed.

End signal.

author: NicVolanschi

repo: Allen

save_path: github-repos/coq/NicVolanschi-Allen


text:
Require Import syntax.
Require Import partial.
Require Import namesAndTypes.
Require Import heap.
Require Import classTable.
Require Import wf_env.

Import ConcreteEverything.

Section Globals.
  Variable P : Program.

  Require Import Coq.Lists.List.

  Print sig.

  Definition global_heap_lst (lst: varDefs) : (* Heap_type * *)Gamma_type * Env_type.
    induction lst.
    exact ((* p_heap.emptyPartFunc,  *)p_gamma.emptyPartFunc, p_env.emptyPartFunc).
    destruct IHlst.
    (* destruct p. *)
    destruct a.
    rename c into C.
    (* rename h into H. *)
    rename e into L.
    rename p into Gamma.
    (* set (o_fresh := ConcreteNamesAndTypes.vn.constructFresh (p_heap.domain H)). *)
    (* destruct o_fresh as [o  o_fresh_proof]. *)

    (* set (flds := fieldsList P C). *)
    (* set (FM := p_FM.newPartFunc flds FM_null). *)
    (* set (heapVal := obj C FM). *)
    split.
    (* split. *)
    (* exact (p_heap.updatePartFunc H o heapVal ). *)
    exact (p_gamma.updatePartFunc Gamma v (typt_class C)).
    exact (p_env.updatePartFunc L v envNull).
  Defined.

  Definition globalEnv (P: Program) : (* Heap_type *  *)Gamma_type * Env_type  :=
    global_heap_lst (globals P).

  (* Theorem WF_globals: *)
  (*   let (p, L) := globalEnv P in let (H, Gamma) := p in WF_Env P H Gamma L. *)
  (*   destruct P. *)
  (*   set (P' := {| *)
  (*    classDecls := classDecls; *)
  (*    globals := globals; *)
  (*    programBody := programBody; *)
  (*    programBodyIsTerm := programBodyIsTerm |}). *)
  (*   unfold globalEnv. *)
  (*   induction (syntax.globals P'). *)
  (*   simpl. *)
  (*   split. *)
  (*   intro. *)
  (*   intro. *)
  (*   simpl in H. *)
  (*   elim H. *)
  (*   intros. *)
  (*   simpl in H.     *)
  (*   simplify_eq H. *)

  (*   case_eq (global_heap_lst v). *)
  (*   intros. *)
  (*   destruct p. *)
  (*   rename H into hyp. *)
  (*   rename h into H; rename p into Gamma; rename e into L. *)
  (*   simpl. *)
  (*   rewrite hyp. *)
  (*   destruct a. *)
  (*   rename c into C. *)
  (*   rename v0 into x. *)
  (*   rename v into rest. *)
  (*   case_eq (ConcreteNamesAndTypes.vn.constructFresh (p_heap.domain H)). *)
  (*   intros o o_fresh. *)
  (*   intro dummy; clear dummy. *)

  (*   split. *)
  (*   rewrite hyp in IHv. *)
  (*   destruct IHv. *)
  (*   apply subset_preserved. *)
  (*   assumption. *)

End Globals.

author: aleloi

repo: lacasa-mechanized