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

ProofByReflection: some copyediting

Browse source
This commit is contained in:
Adam Chlipala 2018-03-06 20:29:57 -05:00
parent 712aacf9de
commit 078e29f8a9
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
ProofByReflection.v
View file

@ -163,7 +163,7 @@ Print true_galore.
* *
* To write a reflective procedure for this class of goals, we will need to get * To write a reflective procedure for this class of goals, we will need to get
* into the actual "reflection" part of "proof by reflection." It is impossible * into the actual "reflection" part of "proof by reflection." It is impossible
* to case-analyze a [Prop] in any way in Gallina. We must_reify_ [Prop] into * to case-analyze a [Prop] in any way in Gallina. We must _reify_ [Prop] into
* some type that we _can_ analyze. This inductive type is a good candidate: *) * some type that we _can_ analyze. This inductive type is a good candidate: *)
(* begin thide *) (* begin thide *)
@ -484,7 +484,7 @@ Ltac reify_set E :=
let e1 := reify_set E1 in let e1 := reify_set E1 in
let e2 := reify_set E2 in let e2 := reify_set E2 in
constr:(Union e1 e2) constr:(Union e1 e2)
| _ => let pf := constr:(eq_refl : E = {}) in constr:(Literal []) | _ => let pf := constr:(E = {}) in constr:(Literal [])
(* The twist is in this case: we instantiate all unification variables with (* The twist is in this case: we instantiate all unification variables with
* the empty set. It's a sound proof step, and it so happens that we only * the empty set. It's a sound proof step, and it so happens that we only
* call this tactic in spots where this heuristic makes sense. *) * call this tactic in spots where this heuristic makes sense. *)
@ -596,10 +596,10 @@ Section my_tauto.
Require Import ListSet. Require Import ListSet.
(* The [eq_nat_dec] below is a richly typed equality test on [nat]s. We'll (* The [eq_nat_dec] below is a richly typed equality test on [nat]s. We'll
* get to the ideas behind it next week. *) * get to the ideas behind it in a later class. *)
Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s. Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s.
(* We define what it means for all members of an variable set to represent (* We define what it means for all members of a variable set to represent
* true propositions, and we prove some lemmas about this notion. *) * true propositions, and we prove some lemmas about this notion. *)
Fixpoint allTrue (s : set propvar) : Prop := Fixpoint allTrue (s : set propvar) : Prop :=