diff --git a/ProofChecker/IntBasedChecker.v b/ProofChecker/IntBasedChecker.v index 8e1cbe07..0f90f29d 100644 --- a/ProofChecker/IntBasedChecker.v +++ b/ProofChecker/IntBasedChecker.v @@ -37,11 +37,11 @@ Variable checkInt : Sig -> rawSymInt -> option symInt. Fixpoint processInt (ri : rawTrsInt) : option (list symInt) := match ri with | nil => Some nil - | cons i is => + | cons i si => match checkInt (fst i) (snd i) with | None => None | Some fi => - match processInt is with + match processInt si with | None => None | Some fis => Some (fi :: fis) end diff --git a/Term/Lambda/LAlpha.v b/Term/Lambda/LAlpha.v index ea844dd3..9aef37e9 100644 --- a/Term/Lambda/LAlpha.v +++ b/Term/Lambda/LAlpha.v @@ -1289,7 +1289,7 @@ while [subs (comp s1 s2) u = Lam y (Var x)] since [comp s1 s2 x = s2 y (** [S*] is a quasi-ordering. *) - Global Instance atc_preorder : PreOrder (S*). + Global Instance atc_preorder : PreOrder (S* ). Proof. split. @@ -1303,7 +1303,7 @@ while [subs (comp s1 s2) u = Lam y (Var x)] since [comp s1 s2 x = s2 y Variable S_aeq : Proper (aeq ==> aeq ==> impl) S. - Global Instance atc_aeq : Proper (aeq ==> aeq ==> impl) (S*). + Global Instance atc_aeq : Proper (aeq ==> aeq ==> impl) (S* ). Proof. intros x x' xx' y y' yy' h. revert x y h x' xx' y' yy'. @@ -1314,7 +1314,7 @@ while [subs (comp s1 s2) u = Lam y (Var x)] since [comp s1 s2 x = s2 y Qed. (*COQ: if removed, Coq fails in LComp*) - Global Instance atc_aeq_iff : Proper (aeq ==> aeq ==> iff) (S*). + Global Instance atc_aeq_iff : Proper (aeq ==> aeq ==> iff) (S* ). Proof. intros x x' xx' y y' yy'. split; intro h; eapply atc_aeq. @@ -1342,7 +1342,7 @@ while [subs (comp s1 s2) u = Lam y (Var x)] since [comp s1 s2 x = s2 y Variable subs_S : Proper (Logic.eq ==> S ==> S) subs. - Global Instance subs_atc : Proper (Logic.eq ==> S* ==> S*) subs. + Global Instance subs_atc : Proper (Logic.eq ==> S* ==> S* ) subs. Proof. intros s s' ss' x y xy. subst s'. revert x y xy. induction 1. @@ -1353,7 +1353,7 @@ while [subs (comp s1 s2) u = Lam y (Var x)] since [comp s1 s2 x = s2 y (*REMOVE?*) Global Instance rename_atc : - Proper (Logic.eq ==> Logic.eq ==> S* ==> S*) rename. + Proper (Logic.eq ==> Logic.eq ==> S* ==> S* ) rename. Proof. intros x x' xx' y y' yy' u u' uu'. unfold Def.rename. @@ -1390,7 +1390,7 @@ while [subs (comp s1 s2) u = Lam y (Var x)] since [comp s1 s2 x = s2 y apply at_step. mon. apply at_aeq. mon. trans (Lam x v); hyp. Qed. - Global Instance App_atc : Monotone S -> Proper (S* ==> S* ==> S*) App. + Global Instance App_atc : Monotone S -> Proper (S* ==> S* ==> S* ) App. Proof. intros m u u' uu' v v' vv'. trans (App u' v). @@ -1402,7 +1402,7 @@ while [subs (comp s1 s2) u = Lam y (Var x)] since [comp s1 s2 x = s2 y apply at_step. mon. apply at_aeq. mon. trans (App u' v); hyp. Qed. - Global Instance Lam_atc : Monotone S -> Proper (Logic.eq ==> S* ==> S*) Lam. + Global Instance Lam_atc : Monotone S -> Proper (Logic.eq ==> S* ==> S* ) Lam. Proof. intros m x x' xx' u u' uu'. subst x'. revert u u' uu'. induction 1. diff --git a/Term/Lambda/LComp.v b/Term/Lambda/LComp.v index 3276d00f..e24be533 100644 --- a/Term/Lambda/LComp.v +++ b/Term/Lambda/LComp.v @@ -350,9 +350,9 @@ Module Make (Export CP : CP_Struct). (** Alpha-transitive closure of [=>R]. *) - Infix "=>R*" := (R_aeq*) (at level 70). + Infix "=>R*" := (R_aeq* ) (at level 70). - Notation satc := (subs_rel (R_aeq*)). + Notation satc := (subs_rel (R_aeq* )). Lemma subs_satc u s s' : satc (fv u) s s' -> subs s u =>R* subs s' u. @@ -574,7 +574,7 @@ Module Make (Export CP : CP_Struct). rewrite <- i1. apply clos_aeq_intro_refl. hyp. rewrite i2. (*COQ: rewrite <- v0v does not work*) gen (proper_atc P_aeq P_red); intro P_reds. - assert (h : Proper (Logic.eq ==> R_aeq* ==> aeq ==> R_aeq*) subs_single). + assert (h : Proper (Logic.eq ==> R_aeq* ==> aeq ==> R_aeq* ) subs_single). apply subs_single_mon_preorder_aeq; class. rewrite <- v0v. hyp. (* app_r *) rewrite ww', i1. apply IH. diff --git a/Term/Lambda/LCompInt.v b/Term/Lambda/LCompInt.v index 551e0f07..47797037 100644 --- a/Term/Lambda/LCompInt.v +++ b/Term/Lambda/LCompInt.v @@ -115,7 +115,7 @@ Module Make (Export ST : ST_Struct) (*COQ: why is it needed?*) Infix "=>R" := (clos_aeq (clos_mon Rh)). - Infix "=>R*" := (R_aeq*). + Infix "=>R*" := (R_aeq* ). (****************************************************************************) (** ** Properties of [supterm_acc]. *) diff --git a/Util/Relation/InfSeq.v b/Util/Relation/InfSeq.v index 5b2860e2..8fe06a5d 100644 --- a/Util/Relation/InfSeq.v +++ b/Util/Relation/InfSeq.v @@ -184,8 +184,8 @@ such that [f i = a] *) Let d := 0. - Definition prefix i := let is := indices i0 in - let n := length is in if lt_dec i n then nth i is d else i0 + g (i - n). + Definition prefix i := let si := indices i0 in + let n := length si in if lt_dec i n then nth i si d else i0 + g (i - n). Lemma prefix_correct : (forall i, f (i0 + g i) = a) -> (forall i, f (prefix i) = a). @@ -201,8 +201,8 @@ such that [f i = a] *) (forall i, g i < g (S i)) -> (forall i, prefix i < prefix (S i)). Proof. - intros hg i. unfold prefix. set (is := indices i0). - set (n := length is). destruct (lt_dec (S i) n); destruct (lt_dec i n). + intros hg i. unfold prefix. set (si := indices i0). + set (n := length si). destruct (lt_dec (S i) n); destruct (lt_dec i n). apply Sorted_nth. class. apply indices_Sorted. hyp. hyp. lia. lia. assert (n=S i). lia. subst. rewrite H, Nat.sub_diag. ded (nth_In d l). destruct (In_indices_aux_elim H0). inversion H1. @@ -215,15 +215,15 @@ such that [f i = a] *) (forall i, f i = a -> exists j, i = prefix j). Proof. - intros hg i e. set (is := indices i0). set (n := length is). - assert (n <= i0). unfold n, is. apply indices_length. + intros hg i e. set (si := indices i0). set (n := length si). + assert (n <= i0). unfold n, si. apply indices_length. destruct (lt_ge_dec i i0). (* i < i0 *) ded (indices_complete l e). destruct (In_nth d H0) as [j [h1 h2]]. - exists j. unfold prefix. fold is. fold n. destruct (lt_dec j n). + exists j. unfold prefix. fold si. fold n. destruct (lt_dec j n). hyp. contr. (* i >= i0 *) - destruct (hg _ g0 e) as [j hj]. exists (n+j). unfold prefix. fold is. + destruct (hg _ g0 e) as [j hj]. exists (n+j). unfold prefix. fold si. fold n. destruct (lt_dec (n+j) n). lia. assert (s : n+j-n=j). lia. rewrite s. hyp. Qed.