Quelle Case22.v Sprache: Coq

(* Check typing in the presence of let-in in inductive arity *)

Inductive I : let a := 1 in a=a -> let b := 2 in Type := C : I (eq_refl).
Lemma a : forall x:I eq_refl, match x in I a b c return b = b with C => eq_refl end = eq_refl.
intro.
match goal with |- ?c => let x := eval cbv in c in change x end.
Abort.

Check forall x:I eq_refl, match x in I x return x = x with C => eq_refl end = eq_refl.

(* This is bug #3210 *)

Inductive I' : let X := Set in X :=
| C' : I'.

Definition foo (x : I') : bool :=
  match x with
  C' => true
  end.

(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *)

Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type :=
  E2 : I2 A nat.

Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
  E2 _ => (0,0,(0,0))
  end.

(* This used to succeed in 8.3, 8.4 and 8.5beta1 *)

Inductive IND : forall X:Type, let Y:=X in Type :=
  CONSTR : IND True.

Definition F (x:IND True) (A:Type) :=
  (* This failed in 8.5beta2 though it should have been accepted *)
  match x in IND X Y return Y with
  CONSTR => Logic.I
  end.

Theorem paradox : False.
  (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
Fail Proof (F C False).
Abort.

(* Another bug found in November 2015 (a substitution was wrongly
   reversed at pretyping level) *)

Inductive Ind (A:Type) :
  let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type :=
  Constr : Ind A nat.

Check fun x:Ind bool nat =>
  match x in Ind _ X Y Z return Z with
  | Constr _ => (true,0)
  end.

(* A vm_compute bug (the type of constructors was not supposed to
   contain local definitions before proper parameters) *)

Inductive Ind2 (b:=1) (c:nat) : Type :=
  Constr2 : Ind2 c.

Eval vm_compute in Constr2 2.

(* A bug introduced in ade2363 (similar to #5322 and #5324). This
   commit started to see that some List.rev was wrong in the "var"
   case of a pattern-matching problem but it failed to see that a
   transformation from a list of arguments into a substitution was
   still needed. *)

(* The order of real arguments was made wrong by ade2363 in the "var"
   case of the compilation of "match" *)

Inductive IND2 : forall X Y:Type, Type :=
  CONSTR2 : IND2 unit Empty_set.

Check fun x:IND2 bool nat =>
  match x in IND2 a b return a with
  | y => _
  end = true.

(* From January 2017, using the proper function to turn arguments into
   a substitution up to a context possibly containing let-ins, so that
   the following, which was wrong also before ade2363, now works
   correctly *)

Check fun x:Ind bool nat =>
  match x in Ind _ X Y Z return Z with
  | y => (true,0)
  end.

(* A check that multi-implicit arguments work *)

Check fun x : {True}+{False} => match x with left _ _ => 0 | right _ _ => 1 end.
Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end.

(* Check that Asymmetric Patterns does not apply to the in clause *)

Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a.
Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end.
Set Asymmetric Patterns.
Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end.
Unset Asymmetric Patterns.

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.