Quelle bug_3481.v Sprache: Coq

Set Implicit Arguments.

Module NonPrim.
Local Set Nonrecursive Elimination Schemes.
Record prodwithlet (A B : Type) : Type :=
  pair' { fst : A; fst' := fst; snd : B }.

Definition letreclet (p : prodwithlet nat nat) :=
  let (x, x', y) := p in x + y.

Definition pletreclet (p : prodwithlet nat nat) :=
  let 'pair' x x' y := p in x + y + x'.

Definition pletreclet2 (p : prodwithlet nat nat) :=
  let 'pair' x y := p in x + y.

Check (pair 0 0).
End NonPrim.

Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Local Set Nonrecursive Elimination Schemes.
Local Set Primitive Projections.

Record prod (A B : Type) : Type :=
  pair { fst : A; snd : B }.

Print prod_rect.

(* What I really want: *)
Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
           (p : prod A B) : P p
  := u (fst p) (snd p).

Definition conv : @prod_rect = @prod_rect'.
Proof. reflexivity. Defined.

Definition imposs :=
  (fun A B P f (p : prod A B) => match p as p0 return P p0 with
                                   | {| fst := x ; snd := x0 |} => f x x0
                                 end).

Definition letrec (p : prod nat nat) :=
  let (x, y) := p in x + y.
Eval compute in letrec (pair 1 5).

Goal forall p : prod nat nat, letrec p = fst p + snd p.
Proof.
  reflexivity.
  Undo.
  intros p.
  case p. simpl. unfold letrec. simpl. reflexivity.
Defined.

Eval compute in conv. (* = eq_refl
     : prod_rect = prod_rect' *)

Check eq_refl : @prod_rect = @prod_rect'. (* Toplevel input, characters 6-13:
Error:
The term "eq_refl" has type "prod_rect = prod_rect"
while it is expected to have type "prod_rect = prod_rect'"
(cannot unify "prod_rect" and "prod_rect'"). *)

Record sigma (A : Type) (B : A -> Type) : Type :=
  dpair { pi1 : A ; pi2 : B pi1 }.

quality99%

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