mirror of
https://github.com/achlipala/frap.git
synced 2024-11-28 07:16:20 +00:00
ProofByReflection_template
This commit is contained in:
parent
2334b84505
commit
89b1b74c7b
3 changed files with 562 additions and 1 deletions
|
@ -4,7 +4,7 @@
|
|||
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/
|
||||
* Much of the material comes from CPDT <http://adam.chlipala.net/cpdt/> by the same author. *)
|
||||
|
||||
Require Import List Frap.
|
||||
Require Import Frap.
|
||||
|
||||
Set Implicit Arguments.
|
||||
Set Asymmetric Patterns.
|
||||
|
@ -780,6 +780,8 @@ Ltac position x ls :=
|
|||
end
|
||||
end.
|
||||
|
||||
(* Compute a duplicate-free list of all variables in [P], combining it with
|
||||
* [acc]. *)
|
||||
Ltac vars_in P acc :=
|
||||
match P with
|
||||
| True => acc
|
||||
|
@ -801,6 +803,8 @@ Ltac vars_in P acc :=
|
|||
end
|
||||
end.
|
||||
|
||||
(* Reification of formula [P], with a pregenertaed list [vars] of variables it
|
||||
* may mention *)
|
||||
Ltac reify_tauto' P vars :=
|
||||
match P with
|
||||
| True => Truth
|
||||
|
|
556
ProofByReflection_template.v
Normal file
556
ProofByReflection_template.v
Normal file
|
@ -0,0 +1,556 @@
|
|||
Require Import Frap.
|
||||
|
||||
Set Implicit Arguments.
|
||||
Set Asymmetric Patterns.
|
||||
|
||||
|
||||
(** * Proving Evenness *)
|
||||
|
||||
Inductive isEven : nat -> Prop :=
|
||||
| Even_O : isEven O
|
||||
| Even_SS : forall n, isEven n -> isEven (S (S n)).
|
||||
|
||||
Theorem even_256 : isEven 256.
|
||||
Proof.
|
||||
Admitted.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(** * Reifying the Syntax of a Trivial Tautology Language *)
|
||||
|
||||
Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
|
||||
Proof.
|
||||
tauto.
|
||||
Qed.
|
||||
|
||||
Print true_galore.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(** * A Monoid Expression Simplifier *)
|
||||
|
||||
Section monoid.
|
||||
Variable A : Set.
|
||||
Variable e : A.
|
||||
Variable f : A -> A -> A.
|
||||
|
||||
Infix "+" := f.
|
||||
|
||||
Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c).
|
||||
Hypothesis identl : forall a, e + a = a.
|
||||
Hypothesis identr : forall a, a + e = a.
|
||||
|
||||
Inductive mexp : Set :=
|
||||
| Ident : mexp
|
||||
| Var : A -> mexp
|
||||
| Op : mexp -> mexp -> mexp.
|
||||
|
||||
(* Next, we write an interpretation function. *)
|
||||
|
||||
Fixpoint mdenote (me : mexp) : A :=
|
||||
match me with
|
||||
| Ident => e
|
||||
| Var v => v
|
||||
| Op me1 me2 => mdenote me1 + mdenote me2
|
||||
end.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Ltac reify me :=
|
||||
match me with
|
||||
| e => Ident
|
||||
| ?me1 + ?me2 =>
|
||||
let r1 := reify me1 in
|
||||
let r2 := reify me2 in
|
||||
constr:(Op r1 r2)
|
||||
| _ => constr:(Var me)
|
||||
end.
|
||||
|
||||
(*Ltac monoid :=
|
||||
match goal with
|
||||
| [ |- ?me1 = ?me2 ] =>
|
||||
let r1 := reify me1 in
|
||||
let r2 := reify me2 in
|
||||
change (mdenote r1 = mdenote r2);
|
||||
apply monoid_reflect; simplify
|
||||
end.
|
||||
|
||||
Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d.
|
||||
simplify; monoid.
|
||||
reflexivity.
|
||||
Qed.*)
|
||||
End monoid.
|
||||
|
||||
|
||||
|
||||
(** * Set Simplification for Model Checking *)
|
||||
|
||||
(* Let's take a closer look at model-checking proofs like from last class. *)
|
||||
|
||||
(* Here's a simple transition system, where state is just a [nat], and where
|
||||
* each step subtracts 1 or 2. *)
|
||||
|
||||
Inductive subtract_step : nat -> nat -> Prop :=
|
||||
| Subtract1 : forall n, subtract_step (S n) n
|
||||
| Subtract2 : forall n, subtract_step (S (S n)) n.
|
||||
|
||||
Definition subtract_sys (n : nat) : trsys nat := {|
|
||||
Initial := {n};
|
||||
Step := subtract_step
|
||||
|}.
|
||||
|
||||
Lemma subtract_ok :
|
||||
invariantFor (subtract_sys 5)
|
||||
(fun n => n <= 5).
|
||||
Proof.
|
||||
eapply invariant_weaken.
|
||||
|
||||
apply multiStepClosure_ok.
|
||||
simplify.
|
||||
(* Here we'll see that the Frap libary uses slightly different, optimized
|
||||
* versions of the model-checking relations. For instance, [multiStepClosure]
|
||||
* takes an extra set argument, the _worklist_ recording newly discovered
|
||||
* states. There is no point in following edges out of states that were
|
||||
* already known at previous steps. *)
|
||||
|
||||
(* Now, some more manual iterations: *)
|
||||
eapply MscStep.
|
||||
closure.
|
||||
(* Ew. What a big, ugly set expression. Let's shrink it down to something
|
||||
* more readable, with duplicates removed, etc. *)
|
||||
simplify.
|
||||
(* How does the Frap library do that? Proof by reflection is a big part of
|
||||
* it! Let's develop a baby version of that automation. The full-scale
|
||||
* version is in file Sets.v. *)
|
||||
Abort.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* Back to our example, which we can now finish without calling [simplify] to
|
||||
* reduces trees of union operations. *)
|
||||
(*Lemma subtract_ok :
|
||||
invariantFor (subtract_sys 5)
|
||||
(fun n => n <= 5).
|
||||
Proof.
|
||||
eapply invariant_weaken.
|
||||
|
||||
apply multiStepClosure_ok.
|
||||
simplify.
|
||||
|
||||
(* Now, some more manual iterations: *)
|
||||
eapply MscStep.
|
||||
closure.
|
||||
simplify_set.
|
||||
(* Success! One subexpression shrunk. Now for the other. *)
|
||||
simplify_set.
|
||||
(* Our automation doesn't handle set difference, so we finish up calling the
|
||||
* library tactic. *)
|
||||
simplify.
|
||||
|
||||
eapply MscStep.
|
||||
closure.
|
||||
simplify_set.
|
||||
simplify_set.
|
||||
simplify.
|
||||
|
||||
eapply MscStep.
|
||||
closure.
|
||||
simplify_set.
|
||||
simplify_set.
|
||||
simplify.
|
||||
|
||||
eapply MscStep.
|
||||
closure.
|
||||
simplify_set.
|
||||
simplify_set.
|
||||
simplify.
|
||||
|
||||
model_check_done.
|
||||
|
||||
simplify.
|
||||
linear_arithmetic.
|
||||
Qed.*)
|
||||
|
||||
|
||||
(** * A Smarter Tautology Solver *)
|
||||
|
||||
Definition propvar := nat.
|
||||
|
||||
Inductive formula : Set :=
|
||||
| Atomic : propvar -> formula
|
||||
| Truth : formula
|
||||
| Falsehood : formula
|
||||
| And : formula -> formula -> formula
|
||||
| Or : formula -> formula -> formula
|
||||
| Imp : formula -> formula -> formula.
|
||||
|
||||
Definition asgn := nat -> Prop.
|
||||
|
||||
Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
|
||||
match f with
|
||||
| Atomic v => atomics v
|
||||
| Truth => True
|
||||
| Falsehood => False
|
||||
| And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
|
||||
| Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
|
||||
| Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2
|
||||
end.
|
||||
|
||||
Section my_tauto.
|
||||
Variable atomics : asgn.
|
||||
|
||||
Require Import ListSet.
|
||||
|
||||
Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s.
|
||||
|
||||
Fixpoint allTrue (s : set propvar) : Prop :=
|
||||
match s with
|
||||
| nil => True
|
||||
| v :: s' => atomics v /\ allTrue s'
|
||||
end.
|
||||
|
||||
Theorem allTrue_add : forall v s,
|
||||
allTrue s
|
||||
-> atomics v
|
||||
-> allTrue (add s v).
|
||||
Proof.
|
||||
induct s; simplify; propositional;
|
||||
match goal with
|
||||
| [ |- context[if ?E then _ else _] ] => destruct E
|
||||
end; simplify; propositional.
|
||||
Qed.
|
||||
|
||||
Theorem allTrue_In : forall v s,
|
||||
allTrue s
|
||||
-> set_In v s
|
||||
-> atomics v.
|
||||
Proof.
|
||||
induct s; simplify; equality.
|
||||
Qed.
|
||||
|
||||
Fixpoint forward (f : formula) (known : set propvar) (hyp : formula)
|
||||
(cont : set propvar -> bool) : bool :=
|
||||
match hyp with
|
||||
| Atomic v => cont (add known v)
|
||||
| Truth => cont known
|
||||
| Falsehood => true
|
||||
| And h1 h2 => forward (Imp h2 f) known h1 (fun known' =>
|
||||
forward f known' h2 cont)
|
||||
| Or h1 h2 => forward f known h1 cont && forward f known h2 cont
|
||||
| Imp _ _ => cont known
|
||||
end.
|
||||
|
||||
Fixpoint backward (known : set propvar) (f : formula) : bool :=
|
||||
match f with
|
||||
| Atomic v => if In_dec eq_nat_dec v known then true else false
|
||||
| Truth => true
|
||||
| Falsehood => false
|
||||
| And f1 f2 => backward known f1 && backward known f2
|
||||
| Or f1 f2 => backward known f1 || backward known f2
|
||||
| Imp f1 f2 => forward f2 known f1 (fun known' => backward known' f2)
|
||||
end.
|
||||
End my_tauto.
|
||||
|
||||
Lemma forward_ok : forall atomics hyp f known cont,
|
||||
forward f known hyp cont = true
|
||||
-> (forall known', allTrue atomics known'
|
||||
-> cont known' = true
|
||||
-> formulaDenote atomics f)
|
||||
-> allTrue atomics known
|
||||
-> formulaDenote atomics hyp
|
||||
-> formulaDenote atomics f.
|
||||
Proof.
|
||||
induct hyp; simplify; propositional.
|
||||
|
||||
apply H0 with (known' := add known p).
|
||||
apply allTrue_add.
|
||||
assumption.
|
||||
assumption.
|
||||
assumption.
|
||||
|
||||
eapply H0.
|
||||
eassumption.
|
||||
assumption.
|
||||
|
||||
eapply IHhyp1 in H.
|
||||
simplify; propositional.
|
||||
simplify.
|
||||
eapply IHhyp2.
|
||||
eassumption.
|
||||
assumption.
|
||||
assumption.
|
||||
assumption.
|
||||
assumption.
|
||||
assumption.
|
||||
|
||||
apply andb_true_iff in H; propositional.
|
||||
eapply IHhyp1.
|
||||
eassumption.
|
||||
assumption.
|
||||
assumption.
|
||||
assumption.
|
||||
|
||||
apply andb_true_iff in H; propositional.
|
||||
eapply IHhyp2.
|
||||
eassumption.
|
||||
assumption.
|
||||
assumption.
|
||||
assumption.
|
||||
|
||||
eapply H0.
|
||||
eassumption.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Lemma backward_ok' : forall atomics f known,
|
||||
backward known f = true
|
||||
-> allTrue atomics known
|
||||
-> formulaDenote atomics f.
|
||||
Proof.
|
||||
induct f; simplify; propositional.
|
||||
|
||||
cases (in_dec Nat.eq_dec p known); propositional.
|
||||
eapply allTrue_In.
|
||||
eassumption.
|
||||
unfold set_In.
|
||||
assumption.
|
||||
equality.
|
||||
|
||||
equality.
|
||||
|
||||
apply andb_true_iff in H; propositional.
|
||||
eapply IHf1.
|
||||
eassumption.
|
||||
assumption.
|
||||
|
||||
apply andb_true_iff in H; propositional.
|
||||
eapply IHf2.
|
||||
eassumption.
|
||||
assumption.
|
||||
|
||||
apply orb_true_iff in H; propositional.
|
||||
left.
|
||||
eapply IHf1.
|
||||
eassumption.
|
||||
assumption.
|
||||
right.
|
||||
eapply IHf2.
|
||||
eassumption.
|
||||
assumption.
|
||||
|
||||
eapply forward_ok.
|
||||
eassumption.
|
||||
simplify.
|
||||
eapply IHf2.
|
||||
eassumption.
|
||||
assumption.
|
||||
assumption.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Theorem backward_ok : forall f,
|
||||
backward [] f = true
|
||||
-> forall atomics, formulaDenote atomics f.
|
||||
Proof.
|
||||
simplify.
|
||||
apply backward_ok' with (known := []).
|
||||
assumption.
|
||||
simplify.
|
||||
propositional.
|
||||
Qed.
|
||||
|
||||
(* Find the position of an element in a list. *)
|
||||
Ltac position x ls :=
|
||||
match ls with
|
||||
| [] => constr:(@None nat)
|
||||
| x :: _ => constr:(Some 0)
|
||||
| _ :: ?ls' =>
|
||||
let p := position x ls' in
|
||||
match p with
|
||||
| None => p
|
||||
| Some ?n => constr:(Some (S n))
|
||||
end
|
||||
end.
|
||||
|
||||
(* Compute a duplicate-free list of all variables in [P], combining it with
|
||||
* [acc]. *)
|
||||
Ltac vars_in P acc :=
|
||||
match P with
|
||||
| True => acc
|
||||
| False => acc
|
||||
| ?Q1 /\ ?Q2 =>
|
||||
let acc' := vars_in Q1 acc in
|
||||
vars_in Q2 acc'
|
||||
| ?Q1 \/ ?Q2 =>
|
||||
let acc' := vars_in Q1 acc in
|
||||
vars_in Q2 acc'
|
||||
| ?Q1 -> ?Q2 =>
|
||||
let acc' := vars_in Q1 acc in
|
||||
vars_in Q2 acc'
|
||||
| _ =>
|
||||
let pos := position P acc in
|
||||
match pos with
|
||||
| Some _ => acc
|
||||
| None => constr:(P :: acc)
|
||||
end
|
||||
end.
|
||||
|
||||
(* Reification of formula [P], with a pregenertaed list [vars] of variables it
|
||||
* may mention *)
|
||||
Ltac reify_tauto' P vars :=
|
||||
match P with
|
||||
| True => Truth
|
||||
| False => Falsehood
|
||||
| ?Q1 /\ ?Q2 =>
|
||||
let q1 := reify_tauto' Q1 vars in
|
||||
let q2 := reify_tauto' Q2 vars in
|
||||
constr:(And q1 q2)
|
||||
| ?Q1 \/ ?Q2 =>
|
||||
let q1 := reify_tauto' Q1 vars in
|
||||
let q2 := reify_tauto' Q2 vars in
|
||||
constr:(Or q1 q2)
|
||||
| ?Q1 -> ?Q2 =>
|
||||
let q1 := reify_tauto' Q1 vars in
|
||||
let q2 := reify_tauto' Q2 vars in
|
||||
constr:(Imp q1 q2)
|
||||
| _ =>
|
||||
let pos := position P vars in
|
||||
match pos with
|
||||
| Some ?pos' => constr:(Atomic pos')
|
||||
end
|
||||
end.
|
||||
|
||||
(* Our final tactic implementation is now fairly straightforward. First, we
|
||||
* [intro] all quantifiers that do not bind [Prop]s. Then we reify. Finally,
|
||||
* we call the verified procedure through a lemma. *)
|
||||
|
||||
Ltac my_tauto :=
|
||||
repeat match goal with
|
||||
| [ |- forall x : ?P, _ ] =>
|
||||
match type of P with
|
||||
| Prop => fail 1
|
||||
| _ => intro
|
||||
end
|
||||
end;
|
||||
match goal with
|
||||
| [ |- ?P ] =>
|
||||
let vars := vars_in P (@nil Prop) in
|
||||
let p := reify_tauto' P vars in
|
||||
change (formulaDenote (nth_default False vars) p)
|
||||
end;
|
||||
apply backward_ok; reflexivity.
|
||||
|
||||
(* A few examples demonstrate how the tactic works: *)
|
||||
|
||||
Theorem mt1 : True.
|
||||
Proof.
|
||||
my_tauto.
|
||||
Qed.
|
||||
|
||||
Print mt1.
|
||||
|
||||
Theorem mt2 : forall x y : nat, x = y -> x = y.
|
||||
Proof.
|
||||
my_tauto.
|
||||
Qed.
|
||||
|
||||
Print mt2.
|
||||
|
||||
Theorem mt3 : forall x y z,
|
||||
(x < y /\ y > z) \/ (y > z /\ x < S y)
|
||||
-> y > z /\ (x < y \/ x < S y).
|
||||
Proof.
|
||||
my_tauto.
|
||||
Qed.
|
||||
|
||||
Print mt3.
|
||||
|
||||
Theorem mt4 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
|
||||
Proof.
|
||||
my_tauto.
|
||||
Qed.
|
||||
|
||||
Print mt4.
|
||||
|
||||
Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
|
||||
Proof.
|
||||
tauto.
|
||||
Qed.
|
||||
|
||||
Print mt4'.
|
|
@ -23,6 +23,7 @@ IntroToProofScripting_template.v
|
|||
ModelChecking_template.v
|
||||
ModelChecking.v
|
||||
ProofByReflection.v
|
||||
ProofByReflection_template.v
|
||||
OperationalSemantics_template.v
|
||||
OperationalSemantics.v
|
||||
AbstractInterpretation.v
|
||||
|
|
Loading…
Reference in a new issue