From 8030db0a1705ba9da5bf38c38e231eff1cf184a0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 15 Mar 2017 11:58:45 -0400 Subject: [PATCH 1/2] LogicProgramming_template.v --- LogicProgramming.v | 2 + LogicProgramming_template.v | 282 ++++++++++++++++++++++++++++++++++++ _CoqProject | 1 + 3 files changed, 285 insertions(+) create mode 100644 LogicProgramming_template.v diff --git a/LogicProgramming.v b/LogicProgramming.v index b47f140..6ff7154 100644 --- a/LogicProgramming.v +++ b/LogicProgramming.v @@ -892,6 +892,7 @@ Section autorewrite. Hint Rewrite f_g. Lemma f_f_f' : forall x, f (f (f x)) = f x. + Proof. intros; autorewrite with core. Abort. @@ -919,6 +920,7 @@ Section autorewrite. Hint Rewrite f_g. Lemma f_f_f' : forall x, f (f (f x)) = f x. + Proof. intros; autorewrite with core. Abort. diff --git a/LogicProgramming_template.v b/LogicProgramming_template.v new file mode 100644 index 0000000..2f91708 --- /dev/null +++ b/LogicProgramming_template.v @@ -0,0 +1,282 @@ +(** Formal Reasoning About Programs + * Supplementary Coq material: proof by reflection + * Author: Adam Chlipala + * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ + * Much of the material comes from CPDT by the same author. *) + +Require Import Frap. + +Set Implicit Arguments. + + +(** * Introducing Logic Programming *) + +(* Recall the definition of addition from the standard library. *) + +Definition real_plus := Eval compute in plus. +Print real_plus. + +(* Alternatively, we can define it as a relation. *) + +Inductive plusR : nat -> nat -> nat -> Prop := +| PlusO : forall m, plusR O m m +| PlusS : forall n m r, plusR n m r + -> plusR (S n) m (S r). + +(* Let's prove the correspondence. *) + +Theorem plusR_plus : forall n m r, + plusR n m r + -> r = n + m. +Proof. +Admitted. + +Theorem plus_plusR : forall n m, + plusR n m (n + m). +Proof. +Admitted. + +Example four_plus_three : 4 + 3 = 7. +Proof. + reflexivity. +Qed. + +Print four_plus_three. + +Example four_plus_three' : plusR 4 3 7. +Proof. +Admitted. + +Print four_plus_three'. + +Example five_plus_three : plusR 5 3 8. +Proof. +Admitted. + +(* Demonstrating _backtracking_ *) +Example seven_minus_three : exists x, x + 3 = 7. +Proof. + apply ex_intro with 0. +Abort. + +Example seven_minus_three' : exists x, plusR x 3 7. +Proof. +Admitted. + +(* Backwards! *) +Example seven_minus_four' : exists x, plusR 4 x 7. +Proof. +Admitted. + +Example seven_minus_three'' : exists x, x + 3 = 7. +Proof. +Admitted. + +Example seven_minus_four : exists x, 4 + x = 7. +Proof. +Admitted. + +Example seven_minus_four_zero : exists x, 4 + x + 0 = 7. +Proof. +Admitted. + +Check eq_trans. + +Section slow. + Hint Resolve eq_trans. + + Example zero_minus_one : exists x, 1 + x = 0. + Time eauto 1. + Time eauto 2. + Time eauto 3. + Time eauto 4. + Time eauto 5. + + debug eauto 3. + Abort. +End slow. + +Example from_one_to_zero : exists x, 1 + x = 0. +Proof. +Admitted. + +Example seven_minus_three_again : exists x, x + 3 = 7. +Proof. +Admitted. + +Example needs_trans : forall x y, 1 + x = y + -> y = 2 + -> exists z, z + x = 3. +Proof. +Admitted. + + +(** * Searching for Underconstrained Values *) + +Print Datatypes.length. + +Example length_1_2 : length (1 :: 2 :: nil) = 2. +Proof. +Admitted. + +Print length_1_2. + +Example length_is_2 : exists ls : list nat, length ls = 2. +Proof. +Abort. + +Print Forall. + +Example length_is_2 : exists ls : list nat, length ls = 2 + /\ Forall (fun n => n >= 1) ls. +Proof. +Admitted. + +Print length_is_2. + +Definition sum := fold_right plus O. + +Example length_and_sum : exists ls : list nat, length ls = 2 + /\ sum ls = O. +Proof. +Admitted. + +Print length_and_sum. + +Example length_and_sum' : exists ls : list nat, length ls = 5 + /\ sum ls = 42. +Proof. +Admitted. + +Print length_and_sum'. + +Example length_and_sum'' : exists ls : list nat, length ls = 2 + /\ sum ls = 3 + /\ Forall (fun n => n <> 0) ls. +Proof. +Admitted. + +Print length_and_sum''. + + +(** * Synthesizing Programs *) + +Inductive exp : Set := +| Const (n : nat) +| Var +| Plus (e1 e2 : exp). + +Inductive eval (var : nat) : exp -> nat -> Prop := +| EvalConst : forall n, eval var (Const n) n +| EvalVar : eval var Var var +| EvalPlus : forall e1 e2 n1 n2, eval var e1 n1 + -> eval var e2 n2 + -> eval var (Plus e1 e2) (n1 + n2). + +Hint Constructors eval. + +Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)). +Proof. + auto. +Qed. + +Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8). +Proof. + eauto. +Abort. + +Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8). +Proof. +Admitted. + +Example synthesize1 : exists e, forall var, eval var e (var + 7). +Proof. +Admitted. + +Print synthesize1. + +(* Here are two more examples showing off our program-synthesis abilities. *) + +Example synthesize2 : exists e, forall var, eval var e (2 * var + 8). +Proof. +Admitted. + +Print synthesize2. + +Example synthesize3 : exists e, forall var, eval var e (3 * var + 42). +Proof. +Admitted. + +Print synthesize3. + +Theorem linear : forall e, exists k n, + forall var, eval var e (k * var + n). +Proof. +Admitted. + +Section side_effect_sideshow. + Variable A : Set. + Variables P Q : A -> Prop. + Variable x : A. + + Hypothesis Px : P x. + Hypothesis Qx : Q x. + + Theorem double_threat : exists y, P y /\ Q y. + Proof. + eexists; propositional. + eauto. + eauto. + Qed. +End side_effect_sideshow. + + +(** * More on [auto] Hints *) + +Theorem bool_neq : true <> false. +Proof. +Admitted. + +Section forall_and. + Variable A : Set. + Variables P Q : A -> Prop. + + Hypothesis both : forall x, P x /\ Q x. + + Theorem forall_and : forall z, P z. + Proof. + Admitted. +End forall_and. + + +(** * Rewrite Hints *) + +Section autorewrite. + Variable A : Set. + Variable f : A -> A. + + Hypothesis f_f : forall x, f (f x) = f x. + + Hint Rewrite f_f. + + Lemma f_f_f : forall x, f (f (f x)) = f x. + Proof. + intros; autorewrite with core; reflexivity. + Qed. + + Section garden_path. + Variable g : A -> A. + Hypothesis f_g : forall x, f x = g x. + Hint Rewrite f_g. + + Lemma f_f_f' : forall x, f (f (f x)) = f x. + Proof. + Admitted. + End garden_path. + + Lemma in_star : forall x y, f (f (f (f x))) = f (f y) + -> f x = f (f (f y)). + Proof. + Admitted. + +End autorewrite. diff --git a/_CoqProject b/_CoqProject index 6bb5e66..143485b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -27,6 +27,7 @@ ProofByReflection_template.v OperationalSemantics_template.v OperationalSemantics.v LogicProgramming.v +LogicProgramming_template.v AbstractInterpretation.v LambdaCalculusAndTypeSoundness_template.v LambdaCalculusAndTypeSoundness.v From ab518492033eb167fa8ccbf19e464322c4cd4da5 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 15 Mar 2017 12:01:28 -0400 Subject: [PATCH 2/2] Fix title in comments --- LogicProgramming.v | 2 +- LogicProgramming_template.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LogicProgramming.v b/LogicProgramming.v index 6ff7154..70a0144 100644 --- a/LogicProgramming.v +++ b/LogicProgramming.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Supplementary Coq material: proof by reflection + * Supplementary Coq material: unification and logic programming * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ * Much of the material comes from CPDT by the same author. *) diff --git a/LogicProgramming_template.v b/LogicProgramming_template.v index 2f91708..0a8d816 100644 --- a/LogicProgramming_template.v +++ b/LogicProgramming_template.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Supplementary Coq material: proof by reflection + * Supplementary Coq material: unification and logic programming * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ * Much of the material comes from CPDT by the same author. *)