mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
Change notation to remain compatible with multiple Coq versions
This commit is contained in:
parent
0f72c50df0
commit
f428750fdf
5 changed files with 31 additions and 31 deletions
|
@ -1219,7 +1219,7 @@ Transparent heq himp lift star exis ptsto.
|
||||||
|
|
||||||
(* Guarded predicates *)
|
(* Guarded predicates *)
|
||||||
Definition guarded (P : Prop) (p : hprop) : hprop :=
|
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.
|
Infix "===>" := guarded : sep_scope.
|
||||||
|
|
||||||
|
|
|
@ -1127,7 +1127,7 @@ Qed.
|
||||||
Transparent heq himp lift star exis ptsto.
|
Transparent heq himp lift star exis ptsto.
|
||||||
|
|
||||||
Definition guarded (P : Prop) (p : hprop) : hprop :=
|
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.
|
Infix "===>" := guarded : sep_scope.
|
||||||
|
|
||||||
|
|
|
@ -458,4 +458,4 @@ Arguments N.add: simpl never.
|
||||||
Definition IF_then_else (p q1 q2 : Prop) :=
|
Definition IF_then_else (p q1 q2 : Prop) :=
|
||||||
(p /\ q1) \/ (~p /\ q2).
|
(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).
|
||||||
|
|
|
@ -586,7 +586,7 @@ Module PropositionalWithImplication.
|
||||||
Lemma interp_valid'' : forall p hyps,
|
Lemma interp_valid'' : forall p hyps,
|
||||||
(forall x, In x (varsOf p) -> hyps (Var x) \/ hyps (Not (Var x)))
|
(forall x, In x (varsOf p) -> hyps (Var x) \/ hyps (Not (Var x)))
|
||||||
-> (forall x, 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
|
then valid hyps p
|
||||||
else valid hyps (Not p).
|
else valid hyps (Not p).
|
||||||
Proof.
|
Proof.
|
||||||
|
@ -612,18 +612,18 @@ Module PropositionalWithImplication.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidAndIntro.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
unfold IF_then_else in H3; 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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
unfold IF_then_else in H3; propositional.
|
unfold IF_then_else in H3; propositional.
|
||||||
right; 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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -637,7 +637,7 @@ Module PropositionalWithImplication.
|
||||||
apply ValidHyp.
|
apply ValidHyp.
|
||||||
propositional.
|
propositional.
|
||||||
right; 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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -654,7 +654,7 @@ Module PropositionalWithImplication.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p1).
|
excluded_middle (interp (fun x => hyps (Var x)) p1).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidOrIntro1.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -662,7 +662,7 @@ Module PropositionalWithImplication.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidOrIntro2.
|
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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -672,7 +672,7 @@ Module PropositionalWithImplication.
|
||||||
apply ValidOrElim with p1 p2.
|
apply ValidOrElim with p1 p2.
|
||||||
apply ValidHyp.
|
apply ValidHyp.
|
||||||
propositional.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -683,7 +683,7 @@ Module PropositionalWithImplication.
|
||||||
propositional.
|
propositional.
|
||||||
apply ValidHyp.
|
apply ValidHyp.
|
||||||
propositional.
|
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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -699,7 +699,7 @@ Module PropositionalWithImplication.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidImplyIntro.
|
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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -709,12 +709,12 @@ Module PropositionalWithImplication.
|
||||||
propositional.
|
propositional.
|
||||||
right; propositional.
|
right; propositional.
|
||||||
apply ValidImplyIntro.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
unfold IF_then_else in H3; 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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -731,7 +731,7 @@ Module PropositionalWithImplication.
|
||||||
propositional.
|
propositional.
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidImplyIntro.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -759,7 +759,7 @@ Module PropositionalWithImplication.
|
||||||
induct leftToDo; simplify.
|
induct leftToDo; simplify.
|
||||||
|
|
||||||
rewrite app_nil_r in H.
|
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.
|
apply interp_valid''; first_order.
|
||||||
unfold IF_then_else in H4; propositional.
|
unfold IF_then_else in H4; propositional.
|
||||||
exfalso.
|
exfalso.
|
||||||
|
|
|
@ -433,7 +433,7 @@ Fixpoint varsOf (p : prop) : list var :=
|
||||||
Lemma interp_valid'' : forall p hyps,
|
Lemma interp_valid'' : forall p hyps,
|
||||||
(forall x, In x (varsOf p) -> hyps (Var x) \/ hyps (Not (Var x)))
|
(forall x, In x (varsOf p) -> hyps (Var x) \/ hyps (Not (Var x)))
|
||||||
-> (forall x, 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
|
then valid hyps p
|
||||||
else valid hyps (Not p).
|
else valid hyps (Not p).
|
||||||
Proof.
|
Proof.
|
||||||
|
@ -459,18 +459,18 @@ Proof.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidAndIntro.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
unfold IF_then_else in H3; 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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
unfold IF_then_else in H3; propositional.
|
unfold IF_then_else in H3; propositional.
|
||||||
right; 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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -484,7 +484,7 @@ Proof.
|
||||||
apply ValidHyp.
|
apply ValidHyp.
|
||||||
propositional.
|
propositional.
|
||||||
right; 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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -501,7 +501,7 @@ Proof.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p1).
|
excluded_middle (interp (fun x => hyps (Var x)) p1).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidOrIntro1.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -509,7 +509,7 @@ Proof.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidOrIntro2.
|
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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -519,7 +519,7 @@ Proof.
|
||||||
apply ValidOrElim with p1 p2.
|
apply ValidOrElim with p1 p2.
|
||||||
apply ValidHyp.
|
apply ValidHyp.
|
||||||
propositional.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -530,7 +530,7 @@ Proof.
|
||||||
propositional.
|
propositional.
|
||||||
apply ValidHyp.
|
apply ValidHyp.
|
||||||
propositional.
|
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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -546,7 +546,7 @@ Proof.
|
||||||
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
excluded_middle (interp (fun x => hyps (Var x)) p2).
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidImplyIntro.
|
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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -556,12 +556,12 @@ Proof.
|
||||||
propositional.
|
propositional.
|
||||||
right; propositional.
|
right; propositional.
|
||||||
apply ValidImplyIntro.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
unfold IF_then_else in H3; 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 IHp2; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -578,7 +578,7 @@ Proof.
|
||||||
propositional.
|
propositional.
|
||||||
left; propositional.
|
left; propositional.
|
||||||
apply ValidImplyIntro.
|
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 IHp1; propositional.
|
||||||
apply H.
|
apply H.
|
||||||
apply in_or_app; propositional.
|
apply in_or_app; propositional.
|
||||||
|
@ -606,7 +606,7 @@ Proof.
|
||||||
induct leftToDo; simplify.
|
induct leftToDo; simplify.
|
||||||
|
|
||||||
rewrite app_nil_r in H.
|
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.
|
apply interp_valid''; first_order.
|
||||||
unfold IF_then_else in H4; propositional.
|
unfold IF_then_else in H4; propositional.
|
||||||
exfalso.
|
exfalso.
|
||||||
|
|
Loading…
Reference in a new issue