Quelle intros.v Sprache: 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 y).
- exact nat.
- exact (y=y).
- auto.
Qed.

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

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

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

End Evar.

Module Wildcard.

(* We check that the wildcard internal name does not interfere with
   user fresh names (currently the prefix is "_H") *)

Goal nat -> bool -> nat -> bool.
intros _ ?_H ?_H.
exact _H.
Qed.

End Wildcard.

Module SimplNever.

Fixpoint arrow n X :=
  match n with
  | 0 => X
  | S n => X -> arrow n X
  end.

Arguments arrow : simpl never.

Goal arrow 1 False.
intro H.
exact H.
Qed.

End SimplNever.

quality99%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.