Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Discriminate_HoTT.v Sprache: Coq

Original von: Coq^©

(* -*- 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.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.