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

Use Admitted instead of Qed when the proof contains "admit" to be

Browse source 
compatible with Coq 8.5.
This commit is contained in:
Theophilos Giannakopoulos 2016-02-05 08:31:26 -05:00
parent ab85cc64ba
commit 555dc01231
2 changed files with 16 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
BasicSyntax_template.v
View file

@ -39,7 +39,7 @@ Compute size ex2.
Theorem depth_le_size : forall e, depth e <= size e.
Proof.
admit.
Qed.
Admitted.
(* A silly recursive function: swap the operand orders of all binary operators. *)
Fixpoint commuter (e : arith) : arith :=
@ -57,17 +57,17 @@ Compute commuter ex2.
Theorem size_commuter : forall e, size (commuter e) = size e.
Proof.
admit.
Qed.
Admitted.
Theorem depth_commuter : forall e, depth (commuter e) = depth e.
Proof.
admit.
Qed.
Admitted.
Theorem commuter_inverse : forall e, commuter (commuter e) = e.
Proof.
admit.
Qed.
Admitted.
@ -105,14 +105,14 @@ Theorem substitute_depth : forall replaceThis withThis inThis,
depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
Proof.
admit.
Qed.
Admitted.
(* A silly self-substitution has no effect. *)
Theorem substitute_self : forall replaceThis inThis,
substitute inThis replaceThis (Var replaceThis) = inThis.
Proof.
admit.
Qed.
Admitted.
(* We can do substitution and commuting in either order. *)
Theorem substitute_commuter : forall replaceThis withThis inThis,
@ -120,7 +120,7 @@ Theorem substitute_commuter : forall replaceThis withThis inThis,
= substitute (commuter inThis) replaceThis (commuter withThis).
Proof.
admit.
Qed.
Admitted.
(* *Constant folding* is one of the classic compiler optimizations.
* We repeatedly find opportunities to replace fancier expressions
@ -156,13 +156,13 @@ Fixpoint constantFold (e : arith) : arith :=
Theorem size_constantFold : forall e, size (constantFold e) <= size e.
Proof.
admit.
Qed.
Admitted.
(* Business as usual, with another commuting law *)
Theorem commuter_constantFold : forall e, commuter (constantFold e) = constantFold (commuter e).
Proof.
admit.
Qed.
Admitted.
(* To define a further transformation, we first write a roundabout way of
* testing whether an expression is a constant. *)
@ -207,7 +207,7 @@ Lemma depth_pushMultiplicationInside'_irrelevance0 : forall e multiplyBy,
= depth (pushMultiplicationInside' 0 e).
Proof.
admit.
Qed.
Admitted.
(* Let's prove that pushing-inside has only a small effect on depth,
* considering for now only coefficient 0. *)
@ -215,11 +215,11 @@ Lemma depth_pushMultiplicationInside' : forall e,
depth (pushMultiplicationInside' 0 e) <= S (depth e).
Proof.
admit.
Qed.
Admitted.
Theorem depth_pushMultiplicationInside : forall e,
depth (pushMultiplicationInside e) <= S (depth e).
Proof.
admit.
Qed.
Admitted.
*)

8
Interpreters_template.v
View file

@ -68,7 +68,7 @@ Fixpoint commuter (e : arith) : arith :=
Theorem commuter_ok : forall v e, interp (commuter e) v = interp e v.
Proof.
admit.
Qed.
Admitted.
(* Let's also revisit substitution. *)
Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
@ -103,7 +103,7 @@ Fixpoint doSomeArithmetic (e : arith) : arith :=
Theorem doSomeArithmetic_ok : forall e v, interp (doSomeArithmetic e) v = interp e v.
Proof.
admit.
Qed.
Admitted.
@ -184,7 +184,7 @@ Fixpoint compile (e : arith) : list instruction :=
Theorem compile_ok : forall e v, run (compile e) v nil = interp e v :: nil.
Proof.
admit.
Qed.
Admitted.
@ -280,7 +280,7 @@ Theorem factorial_ok : forall v input,
-> exec factorial v $? "output" = Some (fact input).
Proof.
admit.
Qed.
Admitted.