diff --git a/AbstractInterpretation.v b/AbstractInterpretation.v index 75ee7de..d9206f2 100644 --- a/AbstractInterpretation.v +++ b/AbstractInterpretation.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 8: Abstract Interpretation and Dataflow Analysis + * Chapter 9: Abstract Interpretation and Dataflow Analysis * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v index 5622ebb..72b31a1 100644 --- a/CompilerCorrectness.v +++ b/CompilerCorrectness.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 9: Compiler Correctness + * Chapter 10: Compiler Correctness * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/CompilerCorrectness_template.v b/CompilerCorrectness_template.v index 4e3e52b..a582fdf 100644 --- a/CompilerCorrectness_template.v +++ b/CompilerCorrectness_template.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 9: Compiler Correctness + * Chapter 10: Compiler Correctness * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 2c02807..05f83ba 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 18: Concurrent Separation Logic + * Chapter 19: Concurrent Separation Logic * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/Connecting.v b/Connecting.v index 9c25bbf..8624407 100644 --- a/Connecting.v +++ b/Connecting.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 15: Connecting to Real-World Programming Languages and Platforms + * Chapter 16: Connecting to Real-World Programming Languages and Platforms * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index e81ca1b..57e98d2 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 13: Deep and Shallow Embeddings + * Chapter 14: Deep and Shallow Embeddings * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/HoareLogic.v b/HoareLogic.v index 74a62a0..a73f190 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 12: Hoare Logic: Verifying Imperative Programs + * Chapter 13: Hoare Logic: Verifying Imperative Programs * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v index f3ecd14..7465afb 100644 --- a/LambdaCalculusAndTypeSoundness.v +++ b/LambdaCalculusAndTypeSoundness.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 10: Lambda Calculus and Simple Type Soundness + * Chapter 11: Lambda Calculus and Simple Type Soundness * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/LambdaCalculusAndTypeSoundness_template.v b/LambdaCalculusAndTypeSoundness_template.v index e3af65e..d99ee14 100644 --- a/LambdaCalculusAndTypeSoundness_template.v +++ b/LambdaCalculusAndTypeSoundness_template.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 8: Lambda Calculus and Simple Type Soundness + * Chapter 11: Lambda Calculus and Simple Type Soundness * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/MessagesAndRefinement.v b/MessagesAndRefinement.v index 0817d71..5756fbb 100644 --- a/MessagesAndRefinement.v +++ b/MessagesAndRefinement.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 19: Process Algebra and Behavioral Refinement + * Chapter 20: Process Algebra and Behavioral Refinement * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/ModelChecking.v b/ModelChecking.v index 23ee33d..9367b4b 100644 --- a/ModelChecking.v +++ b/ModelChecking.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 6: Model Checking + * Chapter 7: Model Checking * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/ModelChecking_template.v b/ModelChecking_template.v index 1bb3dc5..f4d91e9 100644 --- a/ModelChecking_template.v +++ b/ModelChecking_template.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 5: Model Checking + * Chapter 7: Model Checking * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/OperationalSemantics.v b/OperationalSemantics.v index 045e6a4..b9442f8 100644 --- a/OperationalSemantics.v +++ b/OperationalSemantics.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 7: Operational Semantics + * Chapter 8: Operational Semantics * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/OperationalSemantics_template.v b/OperationalSemantics_template.v index a76fc6d..1e966e6 100644 --- a/OperationalSemantics_template.v +++ b/OperationalSemantics_template.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 6: Operational Semantics + * Chapter 8: Operational Semantics * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/ProgramDerivation.v b/ProgramDerivation.v index 7422dad..bb0d3c1 100644 --- a/ProgramDerivation.v +++ b/ProgramDerivation.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 16: Deriving Programs from Specifications + * Chapter 17: Deriving Programs from Specifications * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ * Some material borrowed from Fiat *) diff --git a/RuleInduction.v b/RuleInduction.v index 3827350..3b58ade 100644 --- a/RuleInduction.v +++ b/RuleInduction.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * New chapter: inductive relations and rule induction + * Chapter 5: inductive relations and rule induction * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/RuleInduction_template.v b/RuleInduction_template.v new file mode 100644 index 0000000..a13e7b5 --- /dev/null +++ b/RuleInduction_template.v @@ -0,0 +1,617 @@ +Require Import Frap. + + +(** * Finite sets as inductive predicates *) + +Inductive my_favorite_numbers : nat -> Prop := +| ILike17 : my_favorite_numbers 17 +| ILike23 : my_favorite_numbers 23 +| ILike42 : my_favorite_numbers 42. + +Check my_favorite_numbers_ind. + +Theorem favorites_below_50 : forall n, my_favorite_numbers n -> n < 50. +Proof. +Admitted. + + +(** * Transitive closure of relations *) + +Inductive tc {A} (R : A -> A -> Prop) : A -> A -> Prop := +| TcBase : forall x y, R x y -> tc R x y +| TcTrans : forall x y z, tc R x y -> tc R y z -> tc R x z. + +(** ** Less-than reimagined *) + +Definition oneApart (n m : nat) : Prop := + n + 1 = m. + +Definition lt' : nat -> nat -> Prop := tc oneApart. + +Theorem lt'_lt : forall n m, lt' n m -> n < m. +Proof. +Admitted. + +Theorem lt_lt' : forall n m, n < m -> lt' n m. +Proof. +Admitted. + +(** ** Transitive closure is idempotent. *) + +Theorem tc_tc2 : forall A (R : A -> A -> Prop) x y, tc R x y -> tc (tc R) x y. +Proof. +Admitted. + +Theorem tc2_tc : forall A (R : A -> A -> Prop) x y, tc (tc R) x y -> tc R x y. +Proof. +Admitted. + + +(** * Permutation *) + +(* Lifted from the Coq standard library: *) +Inductive Permutation {A} : list A -> list A -> Prop := +| perm_nil : + Permutation [] [] +| perm_skip : forall x l l', + Permutation l l' -> Permutation (x::l) (x::l') +| perm_swap : forall x y l, + Permutation (y::x::l) (x::y::l) +| perm_trans : forall l l' l'', + Permutation l l' -> Permutation l' l'' -> Permutation l l''. + +Theorem Permutation_rev : forall A (ls : list A), + Permutation ls (rev ls). +Proof. +Admitted. + +Theorem Permutation_length : forall A (ls1 ls2 : list A), + Permutation ls1 ls2 -> length ls1 = length ls2. +Proof. +Admitted. + +Theorem Permutation_app : forall A (ls1 ls1' ls2 ls2' : list A), + Permutation ls1 ls1' + -> Permutation ls2 ls2' + -> Permutation (ls1 ++ ls2) (ls1' ++ ls2'). +Proof. +Admitted. + + +(** * Simple propositional logic *) + +Inductive prop := +| Truth +| Falsehood +| And (p1 p2 : prop) +| Or (p1 p2 : prop). + +Inductive valid : prop -> Prop := +| ValidTruth : + valid Truth +| ValidAnd : forall p1 p2, + valid p1 + -> valid p2 + -> valid (And p1 p2) +| ValidOr1 : forall p1 p2, + valid p1 + -> valid (Or p1 p2) +| ValidOr2 : forall p1 p2, + valid p2 + -> valid (Or p1 p2). + +Fixpoint interp (p : prop) : Prop := + match p with + | Truth => True + | Falsehood => False + | And p1 p2 => interp p1 /\ interp p2 + | Or p1 p2 => interp p1 \/ interp p2 + end. + +Theorem interp_valid : forall p, interp p -> valid p. +Proof. +Admitted. + +Theorem valid_interp : forall p, valid p -> interp p. +Proof. +Admitted. + +Fixpoint commuter (p : prop) : prop := + match p with + | Truth => Truth + | Falsehood => Falsehood + | And p1 p2 => And (commuter p2) (commuter p1) + | Or p1 p2 => Or (commuter p2) (commuter p1) + end. + +Theorem valid_commuter_fwd : forall p, valid p -> valid (commuter p). +Proof. +Admitted. + +Theorem valid_commuter_bwd : forall p, valid (commuter p) -> valid p. +Proof. +Admitted. + + + +(* Proofs for an extension I hope we'll get to: + +Fixpoint interp (vars : var -> Prop) (p : prop) : Prop := + match p with + | Truth => True + | Falsehood => False + | Var x => vars x + | And p1 p2 => interp vars p1 /\ interp vars p2 + | Or p1 p2 => interp vars p1 \/ interp vars p2 + | Imply p1 p2 => interp vars p1 -> interp vars p2 + end. + +Theorem valid_interp : forall vars hyps p, + valid hyps p + -> (forall h, hyps h -> interp vars h) + -> interp vars p. +Proof. + induct 1; simplify. + + apply H0. + assumption. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + apply IHvalid2. + propositional. + equality. + apply H2. + assumption. + apply IHvalid3. + propositional. + equality. + apply H2. + assumption. + + apply IHvalid. + propositional. + equality. + apply H0. + assumption. + + propositional. + + excluded_middle (interp vars p); propositional. + (* Note that use of excluded middle is a bit controversial in Coq, + * and we'll generally be trying to avoid it, + * but it helps enough with this example that we don't sweat the details. *) +Qed. + +Lemma valid_weaken : forall hyps1 p, + valid hyps1 p + -> forall hyps2 : prop -> Prop, + (forall h, hyps1 h -> hyps2 h) + -> valid hyps2 p. +Proof. + induct 1; simplify. + + apply ValidHyp. + apply H0. + assumption. + + apply ValidTruthIntro. + + apply ValidFalsehoodElim. + apply IHvalid. + assumption. + + apply ValidAndIntro. + apply IHvalid1. + assumption. + apply IHvalid2. + assumption. + + apply ValidAndElim1 with p2. + apply IHvalid. + assumption. + + apply ValidAndElim2 with p1. + apply IHvalid. + assumption. + + apply ValidOrIntro1. + apply IHvalid. + assumption. + + apply ValidOrIntro2. + apply IHvalid. + assumption. + + apply ValidOrElim with p1 p2. + apply IHvalid1. + assumption. + apply IHvalid2. + first_order. + apply IHvalid3. + first_order. + + apply ValidImplyIntro. + apply IHvalid. + propositional. + right. + apply H0. + assumption. + + apply ValidImplyElim with p1. + apply IHvalid1. + assumption. + apply IHvalid2. + assumption. + + apply ValidExcludedMiddle. +Qed. + +Lemma valid_cut : forall hyps1 p p', + valid hyps1 p + -> forall hyps2, valid hyps2 p' + -> (forall h, hyps1 h -> hyps2 h \/ h = p') + -> valid hyps2 p. +Proof. + induct 1; simplify. + + apply H1 in H. + propositional. + apply ValidHyp. + assumption. + equality. + + apply ValidTruthIntro. + + apply ValidFalsehoodElim. + apply IHvalid; assumption. + + apply ValidAndIntro. + apply IHvalid1; assumption. + apply IHvalid2; assumption. + + apply ValidAndElim1 with p2. + apply IHvalid; assumption. + + apply ValidAndElim2 with p1. + apply IHvalid; assumption. + + apply ValidOrIntro1. + apply IHvalid; assumption. + + apply ValidOrIntro2. + apply IHvalid; assumption. + + apply ValidOrElim with p1 p2. + apply IHvalid1; assumption. + apply IHvalid2. + apply valid_weaken with hyps2. + assumption. + propositional. + first_order. + apply IHvalid3. + apply valid_weaken with hyps2. + assumption. + propositional. + first_order. + + apply ValidImplyIntro. + apply IHvalid. + apply valid_weaken with hyps2. + assumption. + propositional. + first_order. + + apply ValidImplyElim with p1. + apply IHvalid1; assumption. + apply IHvalid2; assumption. + + apply ValidExcludedMiddle. +Qed. + +Fixpoint varsOf (p : prop) : list var := + match p with + | Truth + | Falsehood => [] + | Var x => [x] + | And p1 p2 + | Or p1 p2 + | Imply p1 p2 => varsOf p1 ++ varsOf p2 + end. + +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 + then valid hyps p + else valid hyps (Not p). +Proof. + induct p; unfold IF_then_else; simplify. + + left; propositional. + apply ValidTruthIntro. + + right; propositional. + apply ValidImplyIntro. + apply ValidHyp. + propositional. + + specialize (H x); propositional. + left; propositional. + apply ValidHyp. + assumption. + right; first_order. + apply ValidHyp. + assumption. + + excluded_middle (interp (fun x => hyps (Var x)) p1). + 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)). + 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)). + 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)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + apply ValidImplyIntro. + apply ValidImplyElim with p2. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidAndElim2 with p1. + apply ValidHyp. + propositional. + right; propositional. + assert (IF 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 H2; propositional. + apply ValidImplyIntro. + apply ValidImplyElim with p1. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidAndElim1 with p2. + apply ValidHyp. + propositional. + + 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)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H2; propositional. + 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)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + right; propositional. + apply ValidImplyIntro. + 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)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + apply ValidImplyElim with p1. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidHyp. + propositional. + assert (IF 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. + apply ValidImplyElim with p2. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidHyp. + propositional. + + excluded_middle (interp (fun x => hyps (Var x)) p1). + 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)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + apply valid_weaken with hyps. + assumption. + propositional. + right; propositional. + apply ValidImplyIntro. + assert (IF 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)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H4; propositional. + apply ValidImplyElim with p2. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidImplyElim with p1. + apply ValidHyp. + propositional. + apply valid_weaken with hyps. + assumption. + propositional. + left; propositional. + apply ValidImplyIntro. + assert (IF 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 H2; propositional. + apply ValidFalsehoodElim. + apply ValidImplyElim with p1. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidHyp. + propositional. +Qed. + +Lemma interp_valid' : forall p leftToDo alreadySplit, + (forall x, In x (varsOf p) -> In x (alreadySplit ++ leftToDo)) + -> forall hyps, (forall x, In x alreadySplit -> hyps (Var x) \/ hyps (Not (Var x))) + -> (forall x, hyps (Var x) \/ hyps (Not (Var x)) -> In x alreadySplit) + -> (forall x, hyps (Var x) -> ~hyps (Not (Var x))) + -> (forall vars : var -> Prop, + (forall x, hyps (Var x) -> vars x) + -> (forall x, hyps (Not (Var x)) -> ~vars x) + -> interp vars p) + -> valid hyps p. +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)). + apply interp_valid''; first_order. + unfold IF_then_else in H4; propositional. + exfalso. + apply H4. + apply H3. + propositional. + first_order. + + excluded_middle (In a alreadySplit). + + apply IHleftToDo with alreadySplit; simplify. + apply H in H5. + apply in_app_or in H5. + simplify. + apply in_or_app. + propositional; subst. + propositional. + first_order. + first_order. + first_order. + first_order. + + apply ValidOrElim with (Var a) (Not (Var a)). + apply ValidExcludedMiddle. + + apply IHleftToDo with (alreadySplit ++ [a]); simplify. + apply H in H5. + apply in_app_or in H5. + simplify. + apply in_or_app. + propositional; subst. + left; apply in_or_app; propositional. + left; apply in_or_app; simplify; propositional. + apply in_app_or in H5. + simplify. + propositional; subst. + apply H0 in H6. + propositional. + propositional. + propositional. + invert H5. + apply in_or_app. + simplify. + propositional. + apply in_or_app. + simplify. + first_order. + invert H5. + apply in_or_app. + simplify. + first_order. + propositional. + invert H5. + invert H7. + first_order. + invert H5. + first_order. + apply H3. + first_order. + first_order. + + apply IHleftToDo with (alreadySplit ++ [a]); simplify. + apply H in H5. + apply in_app_or in H5. + simplify. + apply in_or_app. + propositional; subst. + left; apply in_or_app; propositional. + left; apply in_or_app; simplify; propositional. + apply in_app_or in H5. + simplify. + propositional; subst. + apply H0 in H6. + propositional. + propositional. + propositional. + invert H5. + apply in_or_app. + simplify. + first_order. + invert H5. + apply in_or_app. + simplify. + propositional. + apply in_or_app. + simplify. + first_order. + propositional. + invert H7. + invert H7. + invert H5. + first_order. + first_order. + apply H3. + first_order. + first_order. +Qed. + +Theorem interp_valid : forall p, + (forall vars, interp vars p) + -> valid (fun _ => False) p. +Proof. + simplify. + apply interp_valid' with (varsOf p) []; simplify; first_order. +Qed. +*) diff --git a/SeparationLogic.v b/SeparationLogic.v index f27a01c..492ac35 100644 --- a/SeparationLogic.v +++ b/SeparationLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 14: Separation Logic + * Chapter 15: Separation Logic * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/SessionTypes.v b/SessionTypes.v index 6bf17bf..f11a70a 100644 --- a/SessionTypes.v +++ b/SessionTypes.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 20: Session Types + * Chapter 21: Session Types * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/SharedMemory.v b/SharedMemory.v index 3552e1a..68f3df4 100644 --- a/SharedMemory.v +++ b/SharedMemory.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 17: Operational Semantics for Shared-Memory Concurrency + * Chapter 18: Operational Semantics for Shared-Memory Concurrency * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/TransitionSystems.v b/TransitionSystems.v index 8fee239..6cb1d9f 100644 --- a/TransitionSystems.v +++ b/TransitionSystems.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 5: Transition Systems + * Chapter 6: Transition Systems * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/TransitionSystems_template.v b/TransitionSystems_template.v index 2661e28..6b1e931 100644 --- a/TransitionSystems_template.v +++ b/TransitionSystems_template.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 4: Transition Systems + * Chapter 6: Transition Systems * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/TypesAndMutation.v b/TypesAndMutation.v index 769cffa..5da5627 100644 --- a/TypesAndMutation.v +++ b/TypesAndMutation.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 11: Types and Mutation + * Chapter 12: Types and Mutation * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/_CoqProject b/_CoqProject index ed8f86a..4300b13 100644 --- a/_CoqProject +++ b/_CoqProject @@ -12,32 +12,33 @@ FrapWithoutSets.v Frap.v BasicSyntax_template.v BasicSyntax.v -Polymorphism.v Polymorphism_template.v -DataAbstraction.v +Polymorphism.v DataAbstraction_template.v +DataAbstraction.v Interpreters_template.v Interpreters.v FirstClassFunctions_template.v FirstClassFunctions.v +RuleInduction_template.v RuleInduction.v TransitionSystems_template.v TransitionSystems.v -IntroToProofScripting.v IntroToProofScripting_template.v +IntroToProofScripting.v ModelChecking_template.v ModelChecking.v -ProofByReflection.v ProofByReflection_template.v +ProofByReflection.v OperationalSemantics_template.v OperationalSemantics.v -LogicProgramming.v LogicProgramming_template.v +LogicProgramming.v AbstractInterpretation.v -CompilerCorrectness.v CompilerCorrectness_template.v -SubsetTypes.v +CompilerCorrectness.v SubsetTypes_template.v +SubsetTypes.v LambdaCalculusAndTypeSoundness_template.v LambdaCalculusAndTypeSoundness.v DependentInductiveTypes_template.v diff --git a/frap_book.tex b/frap_book.tex index 2408c55..675e4a2 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -1269,8 +1269,10 @@ The most important extension to the interpreter is that it now takes in a valuat \denote{\phi_1 \Rightarrow \phi_2}v &=& \denote{\phi_1}v \Rightarrow \denote{\phi_2}v \end{eqnarray*} +To indicate that $\phi$ is a \emph{tautology}\index{tautology} (that is, true under any values of the variables), we write $\denote{\phi}$, as a kind of abuse of notation expanding to $\forall v. \; \denote{\phi}v$. + \begin{theorem}[Soundness] - If $\vdash \phi$, then $\denote{\phi}v$ for any $v$. + If $\vdash \phi$, then $\denote{\phi}$. \end{theorem} \begin{proof} By appeal to Lemma \ref{valid_interp'}. @@ -1287,7 +1289,7 @@ The other direction, completeness, is quite a bit more involved, and indeed its The basic idea is to do a proof by exhaustive case analysis over the truth values of all propositional variables $p$ that appear in a formula. \begin{theorem}[Completeness] - If $\denote{\phi}v$ for all $v$, then $\vdash \phi$. + If $\denote{\phi}$, then $\vdash \phi$. \end{theorem} \begin{proof} By appeal to Lemma \ref{interp_valid'}.