Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: misc_extended.v Sprache: Coq

Original von: Coq^©

Require Import ssreflect.

Require Import List.

Lemma test_elim_pattern_1 : forall A (l:list A), l ++ nil = l.
Proof.
intros A.
elim/list_ind => [^~ 1 ].
  by [].
match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end.
Abort.

Lemma test_elim_pattern_2 : forall A (l:list A), l ++ nil = l.
Proof.
intros. elim: l => [^~ 1 ].
  by [].
match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end.
Abort.

Lemma test_elim_pattern_3 : forall A (l:list A), l ++ nil = l.
Proof.
intros. elim: l => [ | x l' IH ].
  by [].
match goal with |- (x :: l') ++ nil = x :: l' => idtac end.
Abort.

Generalizable Variables A.

Class Inhab (A:Type) : Type :=
  { arbitrary : A }.

Lemma test_intro_typeclass_1 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
Proof.
move =>> H.
  match goal with |- _ = _ => idtac end.
Abort.

Lemma test_intro_typeclass_2 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary.
Proof.
move =>> H.
  match goal with |- _ = _ => idtac end.
Abort.

Lemma test_intro_temporary_1 : forall A (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
Proof.
move => A + l2.
  match goal with |- forall l1, l2 = nil -> l1 ++ l2 = l1 => idtac end.
Abort.

Lemma test_intro_temporary_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
Proof.
move => > E.
  match goal with |- _ = _ => idtac end.
Abort.

Lemma test_dispatch : (forall x:nat, x= x )/\ (forall y:nat, y = y).
Proof.
intros. split => [ a | b ].
  match goal with |- a = a => by [] end.
match goal with |- b = b => by [] end.
Abort.

Lemma test_tactics_as_view_1 : forall A (l1:list A), nil ++ l1 = l1.
Proof.
move => /ltac:(simpl).
Abort.

Lemma test_tactics_as_view_2 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A).
Proof.
move => A.
(* TODO: I want to do  [split =>.] as a temporary step in setting up my script,
    but this syntax does not seem to be supported. Can't we have an empty ipat?
   Note that I can do [split => [ | ]]*)
split => [| /ltac:(simpl)].
Abort.

Notation "%%" := (ltac:(simpl)) : ssripat_scope.

Lemma test_tactics_as_view_3 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A).
Proof.
move => /ltac:(split) [ | /%% ].
Abort.

¤ Dauer der Verarbeitung: 0.0 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.