pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

For Coq 8.5 compatibility, use [Admitted] instead of [admit]

Browse source
This commit is contained in:
Adam Chlipala 2016-02-09 18:10:58 -05:00
parent 44696bb5b1
commit 4539409e73
2 changed files with 10 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
BasicSyntax_template.v
View file

@ -38,8 +38,7 @@ Compute size ex2.
* Size is an upper bound on depth. *) * Size is an upper bound on depth. *)
Theorem depth_le_size : forall e, depth e <= size e. Theorem depth_le_size : forall e, depth e <= size e.
Proof. Proof.
admit. Admitted.
Qed.
(* A silly recursive function: swap the operand orders of all binary operators. *) (* A silly recursive function: swap the operand orders of all binary operators. *)
Fixpoint commuter (e : arith) : arith := Fixpoint commuter (e : arith) : arith :=
@ -56,18 +55,16 @@ Compute commuter ex2.
Theorem size_commuter : forall e, size (commuter e) = size e. Theorem size_commuter : forall e, size (commuter e) = size e.
Proof. Proof.
admit. Admitted.
Qed.
Theorem depth_commuter : forall e, depth (commuter e) = depth e. Theorem depth_commuter : forall e, depth (commuter e) = depth e.
Proof. Proof.
admit. Admitted.
Qed.
Theorem commuter_inverse : forall e, commuter (commuter e) = e. Theorem commuter_inverse : forall e, commuter (commuter e) = e.
Proof. Proof.
admit. Admitted.
Qed.

13
Interpreters_template.v
View file

@ -67,8 +67,7 @@ Fixpoint commuter (e : arith) : arith :=
* *meanings* of expressions! *) * *meanings* of expressions! *)
Theorem commuter_ok : forall v e, interp (commuter e) v = interp e v. Theorem commuter_ok : forall v e, interp (commuter e) v = interp e v.
Proof. Proof.
admit. Admitted.
Qed.
(* Let's also revisit substitution. *) (* Let's also revisit substitution. *)
Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith := Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
@ -102,8 +101,7 @@ Fixpoint doSomeArithmetic (e : arith) : arith :=
Theorem doSomeArithmetic_ok : forall e v, interp (doSomeArithmetic e) v = interp e v. Theorem doSomeArithmetic_ok : forall e v, interp (doSomeArithmetic e) v = interp e v.
Proof. Proof.
admit. Admitted.
Qed.
@ -183,8 +181,8 @@ Fixpoint compile (e : arith) : list instruction :=
Theorem compile_ok : forall e v, run (compile e) v nil = interp e v :: nil. Theorem compile_ok : forall e v, run (compile e) v nil = interp e v :: nil.
Proof. Proof.
admit. Admitted.
Qed.
@ -279,8 +277,7 @@ Theorem factorial_ok : forall v input,
v $? "input" = Some input v $? "input" = Some input
-> exec factorial v $? "output" = Some (fact input). -> exec factorial v $? "output" = Some (fact input).
Proof. Proof.
admit. Admitted.
Qed.