From f428750fdfed95af82051790e380bc1e0fb2501a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 31 Jan 2022 21:02:31 -0500 Subject: [PATCH] Change notation to remain compatible with multiple Coq versions --- ConcurrentSeparationLogic.v | 2 +- ConcurrentSeparationLogic_template.v | 2 +- FrapWithoutSets.v | 2 +- RuleInduction.v | 28 ++++++++++++++-------------- RuleInduction_template.v | 28 ++++++++++++++-------------- 5 files changed, 31 insertions(+), 31 deletions(-) diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 5c3ed11..3cdd1ec 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -1219,7 +1219,7 @@ Transparent heq himp lift star exis ptsto. (* Guarded predicates *) Definition guarded (P : Prop) (p : hprop) : hprop := - fun h => IF P then p h else emp%sep h. + fun h => IFF P then p h else emp%sep h. Infix "===>" := guarded : sep_scope. diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v index f7ec4e0..9eb44e8 100644 --- a/ConcurrentSeparationLogic_template.v +++ b/ConcurrentSeparationLogic_template.v @@ -1127,7 +1127,7 @@ Qed. Transparent heq himp lift star exis ptsto. Definition guarded (P : Prop) (p : hprop) : hprop := - fun h => IF P then p h else emp%sep h. + fun h => IFF P then p h else emp%sep h. Infix "===>" := guarded : sep_scope. diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v index 8bb3adc..2dc0e1b 100644 --- a/FrapWithoutSets.v +++ b/FrapWithoutSets.v @@ -458,4 +458,4 @@ Arguments N.add: simpl never. Definition IF_then_else (p q1 q2 : Prop) := (p /\ q1) \/ (~p /\ q2). -Notation "'IF' p 'then' q1 'else' q2" := (IF_then_else p q1 q2) (at level 95). +Notation "'IFF' p 'then' q1 'else' q2" := (IF_then_else p q1 q2) (at level 95). diff --git a/RuleInduction.v b/RuleInduction.v index 3b58ade..5be223b 100644 --- a/RuleInduction.v +++ b/RuleInduction.v @@ -586,7 +586,7 @@ Module PropositionalWithImplication. Lemma interp_valid'' : forall p hyps, (forall x, In x (varsOf p) -> hyps (Var x) \/ hyps (Not (Var x))) -> (forall x, hyps (Var x) -> ~hyps (Not (Var x))) - -> IF interp (fun x => hyps (Var x)) p + -> IFF interp (fun x => hyps (Var x)) p then valid hyps p else valid hyps (Not p). Proof. @@ -612,18 +612,18 @@ Module PropositionalWithImplication. excluded_middle (interp (fun x => hyps (Var x)) p2). left; propositional. apply ValidAndIntro. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. unfold IF_then_else in H3; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. unfold IF_then_else in H3; propositional. right; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -637,7 +637,7 @@ Module PropositionalWithImplication. apply ValidHyp. propositional. right; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -654,7 +654,7 @@ Module PropositionalWithImplication. excluded_middle (interp (fun x => hyps (Var x)) p1). left; propositional. apply ValidOrIntro1. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -662,7 +662,7 @@ Module PropositionalWithImplication. excluded_middle (interp (fun x => hyps (Var x)) p2). left; propositional. apply ValidOrIntro2. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -672,7 +672,7 @@ Module PropositionalWithImplication. apply ValidOrElim with p1 p2. apply ValidHyp. propositional. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -683,7 +683,7 @@ Module PropositionalWithImplication. propositional. apply ValidHyp. propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -699,7 +699,7 @@ Module PropositionalWithImplication. excluded_middle (interp (fun x => hyps (Var x)) p2). left; propositional. apply ValidImplyIntro. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -709,12 +709,12 @@ Module PropositionalWithImplication. propositional. right; propositional. apply ValidImplyIntro. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. unfold IF_then_else in H3; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -731,7 +731,7 @@ Module PropositionalWithImplication. propositional. left; propositional. apply ValidImplyIntro. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -759,7 +759,7 @@ Module PropositionalWithImplication. induct leftToDo; simplify. rewrite app_nil_r in H. - assert (IF interp (fun x : var => hyps (Var x)) p then valid hyps p else valid hyps (Not p)). + assert (IFF interp (fun x : var => hyps (Var x)) p then valid hyps p else valid hyps (Not p)). apply interp_valid''; first_order. unfold IF_then_else in H4; propositional. exfalso. diff --git a/RuleInduction_template.v b/RuleInduction_template.v index 7125136..937a5e8 100644 --- a/RuleInduction_template.v +++ b/RuleInduction_template.v @@ -433,7 +433,7 @@ Fixpoint varsOf (p : prop) : list var := Lemma interp_valid'' : forall p hyps, (forall x, In x (varsOf p) -> hyps (Var x) \/ hyps (Not (Var x))) -> (forall x, hyps (Var x) -> ~hyps (Not (Var x))) - -> IF interp (fun x => hyps (Var x)) p + -> IFF interp (fun x => hyps (Var x)) p then valid hyps p else valid hyps (Not p). Proof. @@ -459,18 +459,18 @@ Proof. excluded_middle (interp (fun x => hyps (Var x)) p2). left; propositional. apply ValidAndIntro. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. unfold IF_then_else in H3; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. unfold IF_then_else in H3; propositional. right; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -484,7 +484,7 @@ Proof. apply ValidHyp. propositional. right; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -501,7 +501,7 @@ Proof. excluded_middle (interp (fun x => hyps (Var x)) p1). left; propositional. apply ValidOrIntro1. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -509,7 +509,7 @@ Proof. excluded_middle (interp (fun x => hyps (Var x)) p2). left; propositional. apply ValidOrIntro2. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -519,7 +519,7 @@ Proof. apply ValidOrElim with p1 p2. apply ValidHyp. propositional. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -530,7 +530,7 @@ Proof. propositional. apply ValidHyp. propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -546,7 +546,7 @@ Proof. excluded_middle (interp (fun x => hyps (Var x)) p2). left; propositional. apply ValidImplyIntro. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -556,12 +556,12 @@ Proof. propositional. right; propositional. apply ValidImplyIntro. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. unfold IF_then_else in H3; propositional. - assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + assert (IFF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). apply IHp2; propositional. apply H. apply in_or_app; propositional. @@ -578,7 +578,7 @@ Proof. propositional. left; propositional. apply ValidImplyIntro. - assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + assert (IFF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). apply IHp1; propositional. apply H. apply in_or_app; propositional. @@ -606,7 +606,7 @@ Proof. induct leftToDo; simplify. rewrite app_nil_r in H. - assert (IF interp (fun x : var => hyps (Var x)) p then valid hyps p else valid hyps (Not p)). + assert (IFF interp (fun x : var => hyps (Var x)) p then valid hyps p else valid hyps (Not p)). apply interp_valid''; first_order. unfold IF_then_else in H4; propositional. exfalso.