Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Tauto.v Sprache: Coq

Original von: Coq^©

(** Some tests of patterns containing matchs ending with joker branches.
    Cf. the new form of the [constr_pattern] constructor [PCase]
    in [pretyping/pattern.ml] *)

(* A universal match matcher *)

Ltac kill_match :=
match goal with
   |- context [ match ?x with _ => _ end ] => destruct x
end.

(* A match matcher restricted to a given type : nat *)

Ltac kill_match_nat :=
match goal with
   |- context [ match ?x in nat with _ => _ end ] => destruct x
end.

(* Another way to restrict to a given type : give a branch *)

Ltac kill_match_nat2 :=
match goal with
   |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x
end.

(* This should act only on empty match *)

Ltac kill_match_empty :=
match goal with
   |- context [ match ?x with end ] => destruct x
end.

Lemma test1 (b:bool) : if b then True else O=O.
Proof.
Fail kill_match_nat.
Fail kill_match_nat2.
Fail kill_match_empty.
kill_match. exact I. exact eq_refl.
Qed.

Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end.
Proof.
Fail kill_match_empty.
kill_match_nat. exact I. exact eq_refl.
Qed.

Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end.
Proof.
kill_match_nat2. exact I. exact eq_refl.
Qed.

Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end.
Proof.
kill_match. exact I. exact eq_refl.
Qed.

Lemma test3a (f:False) : match f return Prop with end.
Proof.
kill_match_empty.
Qed.

Lemma test3b (f:False) : match f return Prop with end.
Proof.
kill_match.
Qed.

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.