diff options
Diffstat (limited to 'test-suite/interactive/proof_block.v')
-rw-r--r-- | test-suite/interactive/proof_block.v | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v new file mode 100644 index 00000000..31e34937 --- /dev/null +++ b/test-suite/interactive/proof_block.v @@ -0,0 +1,66 @@ +Goal False /\ True. +Proof. +split. + idtac. + idtac. + exact I. +idtac. +idtac. +exact I. +Qed. + +Lemma baz : (exists n, n = 3 /\ n = 3) /\ True. +Proof. +split. { eexists. split. par: trivial. } +trivial. +Qed. + +Lemma baz1 : (True /\ False) /\ True. +Proof. +split. { split. par: trivial. } +trivial. +Qed. + +Lemma foo : (exists n, n = 3 /\ n = 3) /\ True. +Proof. +split. + { idtac. + unshelve eexists. + { apply 3. } + { split. + { idtac. trivialx. } + { reflexivity. } } } + trivial. +Qed. + +Lemma foo1 : False /\ True. +Proof. +split. + { exact I. } + { exact I. } +Qed. + +Definition banana := true + 4. + +Check banana. + +Lemma bar : (exists n, n = 3 /\ n = 3) /\ True. +Proof. +split. + - idtac. + unshelve eexists. + + apply 3. + + split. + * idtacx. trivial. + * reflexivity. + - trivial. +Qed. + +Lemma baz2 : ((1=0 /\ False) /\ True) /\ False. +Proof. +split. split. split. + - solve [ auto ]. + - solve [ trivial ]. + - solve [ trivial ]. + - exact 6. +Qed.
\ No newline at end of file |