aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-13 18:29:35 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-13 18:29:35 +0100
commitbd76e995548d23100f2dbe7f5d13047402eb8251 (patch)
tree47137799ec7eab4b378c2ea55ef7e06c6d490500 /test-suite
parent2bfa94975ecc58d35637689ef2fd4473e8126c2e (diff)
STM: fix very simple demo
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/interactive/Paral-ITP.v83
1 files changed, 3 insertions, 80 deletions
diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v
index 55ca52bef..658e6856f 100644
--- a/test-suite/interactive/Paral-ITP.v
+++ b/test-suite/interactive/Paral-ITP.v
@@ -7,19 +7,12 @@ Fixpoint fib n := match n with
Ltac sleep n :=
try (cut (fib n = S (fib n)); reflexivity).
-Let time := 15.
-
-(* BEGIN MINI DEMO *)
-(* JUMP TO "JUMP HERE" *)
-
-Require Import ZArith Psatz.
+Let time := 18.
Lemma a : True.
Proof.
sleep time.
idtac.
- assert(forall n m : Z, n + m = m + n)%Z.
- intros; lia.
sleep time.
exact (I I).
Qed.
@@ -29,80 +22,10 @@ Proof.
do 11 (cut Type; [ intro foo; clear foo | exact Type]).
sleep time.
idtac.
- assert(forall n m : Z, n + m = m + n)%Z.
- intros; lia.
- (* change in semantics: Print a. *)
sleep time.
exact a.
-Qed. (* JUMP HERE *)
-
-Lemma work_here : True.
-Proof.
-cut True.
-Print b.
-Abort.
-
-(* END MINI DEMO *)
-
-
-
-Require Import Unicode.Utf8.
-Notation "a ⊃ b" := (a → b) (at level 91, left associativity).
-
-Definition untrue := False.
-
-Section Ex.
-Variable P Q : Prop.
-Implicit Types X Y : Prop.
-Hypothesis CL : forall X Y, (X → ¬Y → untrue) → (¬X ∨ Y).
-
-Lemma Peirce : P ⊃ Q ⊃ P ⊃ P.
-Proof (* using P Q CL. *). (* Uncomment -> more readable *)
-intro pqp.
-
- Remark EM : ¬P ∨ P.
- Proof using P CL.
- intros; apply CL; intros p np.
- Fail progress auto. (* Missing hint *)
-
- (* Try commenting this out *)
- Hint Extern 0 => match goal with
- p : P, np : ¬P |- _ => case (np p)
- end.
-
- auto. (* This line requires the hint above *)
- Qed.
-
-case EM; auto. (* This line requires the hint above *)
Qed.
-End Ex.
-
-Check EM. (* Print EM. *)
-
-
-Axiom exM : forall P, P \/ ~P.
-
-Lemma CPeirce (P Q : Prop) : P ⊃ Q ⊃ P ⊃ P.
-Proof.
-apply Peirce.
-intros.
-case (exM X); auto.
-intro; right.
-case (exM Y); auto; intro.
-case H; auto.
-Qed.
-
-Require Import Recdef.
-
-Definition m (n : nat) := n.
-
-Function f (n : nat) {measure m n} : bool :=
- match n with
- | O => true
- | S x => f (x + 0)
- end.
+Lemma work_here : True.
Proof.
-intros x y _. unfold m.
-rewrite <- plus_n_O. auto.
-Qed.
+exact I.