|
(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter") -*- *)
(* This file tests the discriminate tactic compatibility with HoTT.
The first part of the file will setup a mini HoTT environment.
Afterwards a number of tests are performed. The tests are basically
copied from the Discriminate.v test file. *)
Unset Elimination Schemes.
Set Universe Polymorphism.
Declare ML Module "ltac_plugin".
Global Set Default Proof Mode "Classic".
Notation "x -> y" := (forall (_:x), y) (at level 99, right associativity, y at level 200).
Cumulative Variant paths {A} (a:A) : A -> Type
:= idpath : paths a a.
Arguments idpath {A a} , [A] a.
Scheme paths_ind := Induction for paths Sort Type.
Arguments paths_ind [A] a P f y p.
Notation "x = y :> A" := (@paths A x y) (at level 70, y at next level, no associativity).
Notation "x = y" := (x = y :>_) (at level 70, no associativity).
Register paths as core.identity.type.
Register idpath as core.identity.refl.
Register paths_ind as core.identity.ind.
Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
:= match p with idpath => idpath end.
Arguments inverse {A x y} p : simpl nomatch.
Register inverse as core.identity.sym.
Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
match p, q with idpath, idpath => idpath end.
Arguments concat {A x y z} p q : simpl nomatch.
Register concat as core.identity.trans.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
Arguments ap {A B} f {x y} p.
Register ap as core.identity.congr.
Variant Empty : Type :=.
Register Empty as core.False.type.
Variant Unit : Type := tt.
Register Unit as core.True.type.
Register tt as core.True.I.
Variant Bool : Type := true | false.
Inductive nat : Type := O | S (n:nat).
(*********** Test discriminate tactic below. ***************)
Goal O = S O -> Empty.
discriminate 1.
Qed.
Goal forall H : O = S O, H = H.
discriminate H.
Qed.
Goal O = S O -> Unit.
intros. discriminate H. Qed.
Goal O = S O -> Unit.
intros. Ltac g x := discriminate x. g H. Qed.
Goal (forall x y : nat, x = y -> x = S y) -> Unit.
intros.
try discriminate (H O) || exact tt.
Qed.
Goal (forall x y : nat, x = y -> x = S y) -> Unit.
intros. ediscriminate (H O). instantiate (1:=O). Abort.
(* Check discriminate on types with local definitions *)
Inductive A := B (T := Unit) (x y : Bool) (z := x).
Goal forall x y, B x true = B y false -> Empty.
discriminate.
Qed.
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
