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

Update for Coq 8.9

Browse source
This commit is contained in:
Adam Chlipala 2019-03-04 11:23:01 -05:00
parent e92a697e33
commit e032ab4240
7 changed files with 23 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.gitignore vendored
View file

@ -12,7 +12,7 @@
Makefile.coq
Makefile.coq.conf
*.glob
*.v.d
*.d
*.vo
frap.tgz
.coq-native

2
DeepAndShallowEmbeddings.v
View file

@ -886,7 +886,7 @@ Module DeeperWithFail.
| Stepped (h : heap) (c : cmd result)
| Failed.
Implicit Arguments Failed [result].
Arguments Failed {result}.
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
match c with

2
DeepAndShallowEmbeddings_template.v
View file

@ -731,7 +731,7 @@ Module DeeperWithFail.
| Stepped (h : heap) (c : cmd result)
| Failed.
Implicit Arguments Failed [result].
Arguments Failed {result}.
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
match c with

2
DependentInductiveTypes.v
View file

@ -1217,7 +1217,7 @@ Section split.
Defined.
End split.
Implicit Arguments split [P1 P2].
Arguments split {P1 P2}.
(* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you
* like. *)

2
DependentInductiveTypes_template.v
View file

@ -599,7 +599,7 @@ Section split.
Defined.
End split.
Implicit Arguments split [P1 P2].
Arguments split {P1 P2}.
(* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you
* like. *)

2
FrapWithoutSets.v
View file

@ -1,5 +1,5 @@
Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
Export Ascii String Arith Sets Relations Map Var Invariant Bool ModelCheck.
Require Import List.
Export List ListNotations.
Open Scope string_scope.

12
SharedMemory.v
View file

@ -776,25 +776,25 @@ Inductive boundRunningTime : cmd -> nat -> Prop :=
(* Perhaps surprisingly, there exist commands that have no finite time bounds!
* Mixed-embedding languages often have these counterintuitive properties. *)
Theorem boundRunningTime_not_total : exists c, forall n, ~boundRunningTime c n.
Proof.
Fixpoint scribbly (n : nat) : cmd :=
Fixpoint scribbly (n : nat) : cmd :=
match n with
| O => Return 0
| S n' => _ <- Write n' 0; scribbly n'
end.
Lemma scribbly_time : forall n m,
Lemma scribbly_time : forall n m,
boundRunningTime (scribbly n) m
-> m >= n.
Proof.
Proof.
induct n; invert 1; auto.
invert H2.
specialize (H4 n0).
apply IHn in H4.
linear_arithmetic.
Qed.
Qed.
Theorem boundRunningTime_not_total : exists c, forall n, ~boundRunningTime c n.
Proof.
exists (n <- Read 0; scribbly n); propositional.
invert H.
specialize (H4 (S n2)).