pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for this week's lectures

Browse source
This commit is contained in:
Adam Chlipala 2021-04-11 13:32:38 -04:00
parent 45124f3686
commit 899b3dee24
5 changed files with 52 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
DependentInductiveTypes.v
View file

@ -141,13 +141,10 @@ Section ilist.
| Cons _ h _ => h
end.
(* Unlike in ML, we cannot use inexhaustive pattern matching, because there is
* no conception of a <<Match>> exception to be thrown. In fact, recent
* versions of Coq _do_ allow this, by implicit translation to a [match] that
* considers all constructors; the error message above was generated by an
* older Coq version. It is educational to discover for ourselves the
* encoding that the most recent Coq versions use. We might try using an [in]
* clause somehow. *)
(* Actually, these days, Coq is smart enough to make that definition work!
* However, it will be educational to look at how Coq elaborates this code
* into its core language, where, unlike in ML, all pattern matching must be
* _exhaustive_. We might try using an [in] clause somehow. *)
Fail Fail Definition hd n (ls : ilist (S n)) : A :=
match ls in (ilist (S n)) with
@ -173,13 +170,22 @@ Section ilist.
Check hd'.
Definition hd n (ls : ilist (S n)) : A := hd' ls.
End ilist.
(* We annotate our main [match] with a type that is itself a [match]. We write
* that the function [hd'] returns [unit] when the list is empty and returns the
* carried type [A] in all other cases. In the definition of [hd], we just call
* [hd']. Because the index of [ls] is known to be nonzero, the type checker
* reduces the [match] in the type of [hd'] to [A]. *)
(* We annotate our main [match] with a type that is itself a [match]. We
* write that the function [hd'] returns [unit] when the list is empty and
* returns the carried type [A] in all other cases. In the definition of [hd],
* we just call [hd']. Because the index of [ls] is known to be nonzero, the
* type checker reduces the [match] in the type of [hd'] to [A]. *)
(* In fact, when we "got lucky" earlier with Coq accepting simpler
* definitions, under the hood it was desugaring _almost_ to this one. *)
Definition easy_hd n (ls : ilist (S n)) : A :=
match ls with
| Cons _ h _ => h
end.
Print easy_hd.
End ilist.
(** * The One Rule of Dependent Pattern Matching in Coq *)
@ -330,7 +336,7 @@ Fixpoint expDenote t (e : exp t) : typeDenote t :=
match e with
| NConst n => n
| Plus e1 e2 => expDenote e1 + expDenote e2
| Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
| Eq e1 e2 => if expDenote e1 ==n expDenote e2 then true else false
| BConst b => b
| And e1 e2 => expDenote e1 && expDenote e2
@ -345,10 +351,10 @@ Fixpoint expDenote t (e : exp t) : typeDenote t :=
* less complicated than what we would write in ML or Haskell 98, since we do
* not need to worry about pushing final values in and out of an algebraic
* datatype. The only unusual thing is the use of an expression of the form
* [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has
* [if E then true else false] in the [Eq] case. Remember that [==n] has
* a rich dependent type, rather than a simple Boolean type. Coq's native [if]
* is overloaded to work on a test of any two-constructor type, so we can use
* [if] to build a simple Boolean from the [sumbool] that [eq_nat_dec] returns.
* [if] to build a simple Boolean from the [sumbool] that [==n] returns.
*
* We can implement our old favorite, a constant-folding function, and prove it
* correct. It will be useful to write a function [pairOut] that checks if an
@ -387,10 +393,7 @@ Definition pairOut t (e : exp t) :=
(* With [pairOut] available, we can write [cfold] in a straightforward way.
* There are really no surprises beyond that Coq verifies that this code has
* such an expressive type, given the small annotation burden. In some places,
* we see that Coq's [match] annotation inference is too smart for its own
* good, and we have to turn that inference off with explicit [return]
* clauses. *)
* such an expressive type, given the small annotation burden. *)
Fixpoint cfold t (e : exp t) : exp t :=
match e with
@ -398,14 +401,14 @@ Fixpoint cfold t (e : exp t) : exp t :=
| Plus e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' return exp Nat with
match e1', e2' with
| NConst n1, NConst n2 => NConst (n1 + n2)
| _, _ => Plus e1' e2'
end
| Eq e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' return exp Bool with
match e1', e2' with
| NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
| _, _ => Eq e1' e2'
end
@ -414,7 +417,7 @@ Fixpoint cfold t (e : exp t) : exp t :=
| And e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' return exp Bool with
match e1', e2' with
| BConst b1, BConst b2 => BConst (b1 && b2)
| _, _ => And e1' e2'
end
@ -488,9 +491,6 @@ Proof.
end; simplify); try equality.
Qed.
(* With this example, we get a first taste of how to build automated proofs that
* adapt automatically to changes in function definitions. *)
(** * Interlude: The Convoy Pattern *)
@ -676,7 +676,7 @@ Section present.
End present.
(* Insertion relies on two balancing operations. It will be useful to give types
* to these operations using a relative of the subset types from last chapter.
* to these operations using a relative of the subset types from SubsetTypes.
* While subset types let us pair a value with a proof about that value, here we
* want to pair a value with another non-proof dependently typed value. The
* [sigT] type fills this role. *)
@ -1071,7 +1071,7 @@ Ltac substring :=
destruct N; simplify
end; try linear_arithmetic; eauto; try equality.
Hint Resolve le_n_S : core.
Local Hint Resolve le_n_S : core.
Lemma substring_le : forall s n m,
length (substring n m s) <= m.
@ -1105,7 +1105,7 @@ Proof.
induct s1; substring.
Qed.
Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
Local Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
Lemma substring_app_fst : forall s2 s1 n,
length s1 = n
@ -1151,7 +1151,7 @@ End sumbool_and.
Infix "&&" := sumbool_and (at level 40, left associativity).
Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Section split.
Variables P1 P2 : string -> Prop.
@ -1253,7 +1253,7 @@ Proof.
induct s; substring.
Qed.
Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
Local Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
Lemma substring_stack : forall s n2 m1 m2,
m1 <= m2
@ -1507,7 +1507,7 @@ Proof.
equality.
Qed.
Hint Resolve app_cong : core.
Local Hint Resolve app_cong : core.
(* With these helper functions completed, the implementation of our [matches]
* function is refreshingly straightforward. *)

16
DependentInductiveTypes_template.v
View file

@ -91,14 +91,14 @@ Fixpoint cfold t (e : exp t) : exp t :=
| Plus e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' return exp Nat with
match e1', e2' with
| NConst n1, NConst n2 => NConst (n1 + n2)
| _, _ => Plus e1' e2'
end
| Eq e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' return exp Bool with
match e1', e2' with
| NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
| _, _ => Eq e1' e2'
end
@ -107,7 +107,7 @@ Fixpoint cfold t (e : exp t) : exp t :=
| And e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' return exp Bool with
match e1', e2' with
| BConst b1, BConst b2 => BConst (b1 && b2)
| _, _ => And e1' e2'
end
@ -487,7 +487,7 @@ Ltac substring :=
destruct N; simplify
end; try linear_arithmetic; eauto; try equality.
Hint Resolve le_n_S : core.
Local Hint Resolve le_n_S : core.
Lemma substring_le : forall s n m,
length (substring n m s) <= m.
@ -521,7 +521,7 @@ Proof.
induct s1; substring.
Qed.
Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
Local Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core.
Lemma substring_app_fst : forall s2 s1 n,
length s1 = n
@ -540,7 +540,7 @@ Proof.
induct s1; simplify; subst; simplify; auto.
Qed.
Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
Local Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
(* BOREDOM'S END! *)
@ -563,7 +563,7 @@ End sumbool_and.
Infix "&&" := sumbool_and (at level 40, left associativity).
Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Section split.
Variables P1 P2 : string -> Prop.
@ -863,7 +863,7 @@ Proof.
equality.
Qed.
Hint Resolve app_cong : core.
Local Hint Resolve app_cong : core.
Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=

12
HoareLogic.v
View file

@ -61,7 +61,7 @@ Fixpoint eval (e : exp) (h : heap) (v : valuation) : nat :=
end.
(* Meaning of Boolean expressions *)
Fixpoint beval (b : bexp) (h : heap) (v : valuation) : bool :=
Definition beval (b : bexp) (h : heap) (v : valuation) : bool :=
match b with
| Equal e1 e2 => if eval e1 h v ==n eval e2 h v then true else false
| Less e1 e2 => if eval e2 h v <=? eval e1 h v then false else true
@ -385,10 +385,10 @@ Proof.
ht.
Qed.
Hint Resolve leq_f : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Hint Extern 1 (_ < _) => linear_arithmetic : core.
Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Local Hint Resolve leq_f : core.
Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Local Hint Extern 1 (_ < _) => linear_arithmetic : core.
Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
(* We also register [linear_arithmetic] as a step to try during proof search. *)
(* These invariants are fairly hairy, but probably the best way to understand
@ -472,7 +472,7 @@ Inductive step : heap * valuation * cmd -> heap * valuation * cmd -> Prop :=
a h v
-> step (h, v, Assert a) (h, v, Skip).
Hint Constructors step : core.
Local Hint Constructors step : core.
Definition trsys_of (st : heap * valuation * cmd) := {|
Initial := {st};

10
HoareLogic_template.v
View file

@ -264,10 +264,10 @@ Proof.
ht.
Qed.
Hint Resolve leq_f : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Hint Extern 1 (_ < _) => linear_arithmetic : core.
Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Local Hint Resolve leq_f : core.
Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Local Hint Extern 1 (_ < _) => linear_arithmetic : core.
Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
(* We also register [linear_arithmetic] as a step to try during proof search. *)
Theorem selectionSort_ok :
@ -324,7 +324,7 @@ Inductive step : heap * valuation * cmd -> heap * valuation * cmd -> Prop :=
a h v
-> step (h, v, Assert a) (h, v, Skip).
Hint Constructors step : core.
Local Hint Constructors step : core.
Definition trsys_of (st : heap * valuation * cmd) := {|
Initial := {st};

3
frap_book.tex
View file

@ -3903,7 +3903,6 @@ We call any such fact a \emph{Hoare triple}\index{Hoare triple}, and the overall
\encoding
A first rule for $\skipe$ is easy: anything that was true before is also true after.
$$\infer{\hoare{P}{\skipe}{P}}{}$$
A rule for assignment is slightly more involved: to state what we know is true after, we recall that there existed a prestate satisfying the precondition, which then evolved into the poststate in the expected way.
@ -4045,7 +4044,7 @@ $$\infer{\smallstep{(h, v, \assert{a})}{(h, v, \skipe)}}{
Even an infinite-looping program must satisfy its $\mathsf{assert}$ commands, every time it passes one of them.
For that reason, it's interesting to consider how to show that a command never gets stuck on a false assertion.
We work up to that result with a few intermediate ones.
First, we define \emph{stuck} much the same way as in the last two chapters: a state $(h, v, c)$ is stuck if $c$ is not $\skipe$, but there is also nowhere to step to from this state.
First, we define \emph{stuck} much the same way as in the last three chapters: a state $(h, v, c)$ is stuck if $c$ is not $\skipe$, but there is also nowhere to step to from this state.
An example of a stuck state would be one beginning with an $\mathsf{assert}$ of an assertion that does not hold on $h$ and $v$.
In fact, we can prove that any other state is unstuck, though we won't bother here.