Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: intros.v Sprache: Coq

Original von: Coq^©

(* Thinning introduction hypothesis must be done after all introductions *)
(* Submitted by Guillaume Melquiond (BZ#1000) *)

Goal forall A, A -> True.
intros _ _.
Abort.

(* This did not work until March 2013, because of underlying "red" *)
Goal (fun x => True -> True) 0.
intro H.
Abort.

(* This should still work, with "intro" calling "hnf" *)
Goal (fun f => True -> f 0 = f 0) (fun x => x).
intro H.
match goal with [ |- 0 = 0 ] => reflexivity end.
Abort.

(* Somewhat related: This did not work until March 2013 *)
Goal (fun f => f 0 = f 0) (fun x => x).
hnf.
match goal with [ |- 0 = 0 ] => reflexivity end.
Abort.

(* Fixing behavior of "*" and "**" in branches, so that they do not
   introduce more than what the branch expects them to introduce at most *)
Goal forall n p, n + p = 0.
intros [|*]; intro p.
Abort.

(* Check non-interference of "_" with name generation *)
Goal True -> True -> True.
intros _ ?.
exact H.
Qed.

(* A short test about introduction pattern pat%c *)
Goal (True -> 0=0) -> True /\ False -> 0=0.
intros H (H1%H,_).
exact H1.
Qed.

(* A test about bugs in 8.5beta2 *)
Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
intros H H0 H1.
destruct H0 as (a%H,_).
(* Check that H0 is removed (was bugged in 8.5beta2) *)
Fail clear H0.
(* Check position of newly created hypotheses when using pat%c (was
   left at top in 8.5beta2) *)
match goal with H:_ |- _ => clear H end. (* clear H1:False *)
match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
Qed.

Goal (True -> 0=0) -> True -> 0=0.
intros H H1%H.
exact H1.
Qed.

Goal forall n, n = S n -> 0=0.
intros n H%n_Sn.
destruct H.
Qed.

(* Another check about generated names and cleared hypotheses with
   pat%c patterns *)
Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
intros H (H1,?)%H.
change (1=1) in H0.
exact H1.
Qed.

(* Checking iterated pat%c1...%cn introduction patterns and side conditions *)

Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D.
intros * H H0 H1.
intros H2%H%H0.
- exact H2.
- exact H1.
Qed.

(* Bug found by Enrico *)

Goal forall x : nat, True.
intros y%(fun x => x).
Abort.

(* Fixing a bug in the order of side conditions of a "->" step *)

Goal (True -> 1=0) -> 1=1.
intros ->.
- reflexivity.
- exact I.
Qed.

Goal forall x, (True -> x=0) -> 0=x.
intros x ->.
- reflexivity.
- exact I.
Qed.

(* Fixing a bug when destructing a type with let-ins in the constructor *)

Inductive I := C : let x:=1 in x=1 -> I.
Goal I -> True.
intros [x H]. (* Was failing in 8.5 *)
Abort.

(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up
   to skipping let-ins *)

Goal I -> 1=1.
intros (H).  (* This skips x *)
exact H.
Qed.

Goal I -> 1=1.
Fail intros (x,H,H').
Fail intros [|].
intros (x,H).
exact H.
Qed.

Goal Acc le 0 -> True.
Fail induction 1 as (n,H). (* Induction hypothesis is missing *)
induction 1 as (n,H,IH).
exact Logic.I.
Qed.

(* Make "intro"/"intros" progress on existential variables *)

Module Evar.

Goal exists (A:Prop), A.
eexists.
unshelve (intro x).
- exact nat.
- exact (x=x).
- auto.
Qed.

Goal exists (A:Prop), A.
eexists.
unshelve (intros x).
- exact nat.
- exact (x=x).
- auto.
Qed.

Definition d := ltac:(intro x; exact (x*x)).

Definition d' : nat -> _ := ltac:(intros;exact 0).

End Evar.

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