frap/ProofByReflection_template.v
2022-03-06 14:47:05 -05:00

565 lines
11 KiB
Coq

Require Import Frap.
Set Implicit Arguments.
Set Asymmetric Patterns.
Set Universe Polymorphism.
(** * 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 library 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.
Require Import ListSet.
Section my_tauto.
Variable atomics : asgn.
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 (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 known h1 (fun known' =>
forward known' h2 cont)
| Or h1 h2 => forward known h1 cont && forward known h2 cont
| Imp _ _ => cont known
end.
Compute fun cont => forward [] (Atomic 0) cont.
Compute fun cont => forward [] (Or (Atomic 0) (Atomic 1)) cont.
Compute fun cont => forward [] (Or (Atomic 0) (And (Atomic 1) (Atomic 2))) cont.
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 known f1 (fun known' => backward known' f2)
end.
Compute backward [] (Atomic 0).
Compute backward [0] (Atomic 0).
Compute backward [0; 2] (Or (Atomic 0) (Atomic 1)).
Compute backward [2] (Or (Atomic 0) (Atomic 1)).
Compute backward [2] (Imp (Atomic 0) (Or (Atomic 0) (Atomic 1))).
Compute backward [2] (Imp (Or (Atomic 0) (Atomic 3)) (Or (Atomic 0) (Atomic 1))).
Compute backward [2] (Imp (Or (Atomic 1) (Atomic 0)) (Or (Atomic 0) (Atomic 1))).
End my_tauto.
Lemma forward_ok : forall atomics hyp f known cont,
forward 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.
eassumption.
simplify.
eauto.
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 pregenerated 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'.