diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/CasesDep.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/CasesDep.v')
-rw-r--r-- | test-suite/success/CasesDep.v | 82 |
1 files changed, 54 insertions, 28 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 49bd77fc..29721843 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -38,29 +38,29 @@ Require Import Logic_Type. Section Orderings. Variable U : Type. - + Definition Relation := U -> U -> Prop. Variable R : Relation. - + Definition Reflexive : Prop := forall x : U, R x x. - + Definition Transitive : Prop := forall x y z : U, R x y -> R y z -> R x z. - + Definition Symmetric : Prop := forall x y : U, R x y -> R y x. - + Definition Antisymmetric : Prop := forall x y : U, R x y -> R y x -> x = y. - + Definition contains (R R' : Relation) : Prop := forall x y : U, R' x y -> R x y. Definition same_relation (R R' : Relation) : Prop := contains R R' /\ contains R' R. Inductive Equivalence : Prop := Build_Equivalence : Reflexive -> Transitive -> Symmetric -> Equivalence. - + Inductive PER : Prop := Build_PER : Symmetric -> Transitive -> PER. - + End Orderings. (***** Setoid *******) @@ -105,7 +105,7 @@ Definition Map_setoid := Build_Setoid Map ext Equiv_map_eq. End Maps. -Notation ap := (explicit_ap _ _). +Notation ap := (explicit_ap _ _). (* <Warning> : Grammar is replaced by Notation *) @@ -128,8 +128,8 @@ Axiom eq_Suc : forall n m : posint, n = m -> Suc n = Suc m. Definition pred (n : posint) : posint := match n return posint with - | Z => (* Z *) Z - (* Suc u *) + | Z => (* Z *) Z + (* Suc u *) | Suc u => u end. @@ -141,7 +141,7 @@ Axiom not_eq_Suc : forall n m : posint, n <> m -> Suc n <> Suc m. Definition IsSuc (n : posint) : Prop := match n return Prop with | Z => (* Z *) False - (* Suc p *) + (* Suc p *) | Suc p => True end. Definition IsZero (n : posint) : Prop := @@ -163,7 +163,7 @@ Definition Decidable (A : Type) (R : Relation A) := forall x y : A, R x y \/ ~ R x y. -Record DSetoid : Type := +Record DSetoid : Type := {Set_of : Setoid; prf_decid : Decidable (elem Set_of) (equal Set_of)}. (* example de Dsetoide d'entiers *) @@ -190,7 +190,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci. Section Sig. -Record Signature : Type := +Record Signature : Type := {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}. Variable S : Signature. @@ -268,8 +268,8 @@ Reset equalT. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 return (TERM -> Prop) with - | var v1 => - (*var*) + | var v1 => + (*var*) fun t2 : TERM => match t2 return Prop with | var v2 => @@ -289,12 +289,12 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 end end - + with EqListT (n1 : posint) (l1 : LTERM n1) {struct l1} : forall n2 : posint, LTERM n2 -> Prop := match l1 in (LTERM _) return (forall n2 : posint, LTERM n2 -> Prop) with | nil => - (*nil*) + (*nil*) fun (n2 : posint) (l2 : LTERM n2) => match l2 in (LTERM _) return Prop with | nil => @@ -336,7 +336,7 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 end end - + with EqListT (n1 : posint) (l1 : LTERM n1) {struct l1} : forall n2 : posint, LTERM n2 -> Prop := match l1 return (forall n2 : posint, LTERM n2 -> Prop) with @@ -374,8 +374,8 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 end end - - with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) + + with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) (l2 : LTERM n2) {struct l1} : Prop := match l1 with | nil => match l2 with @@ -401,8 +401,8 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := equal _ op1 op2 /\ EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 | _, _ => False end - - with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) + + with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) (l2 : LTERM n2) {struct l1} : Prop := match l1, l2 with | nil, nil => True @@ -433,16 +433,16 @@ Inductive I : unit -> Type := | C : forall a, I a -> I tt. (* -Definition F (l:I tt) : l = l := +Definition F (l:I tt) : l = l := match l return l = l with | C tt (C _ l') => refl_equal (C tt (C _ l')) end. one would expect that the compilation of F (this involves -some kind of pattern-unification) would produce: +some kind of pattern-unification) would produce: *) -Definition F (l:I tt) : l = l := +Definition F (l:I tt) : l = l := match l return l = l with | C tt l' => match l' return C _ l' = C _ l' with C _ l'' => refl_equal (C tt (C _ l'')) end end. @@ -451,7 +451,7 @@ Inductive J : nat -> Type := | D : forall a, J (S a) -> J a. (* -Definition G (l:J O) : l = l := +Definition G (l:J O) : l = l := match l return l = l with | D O (D 1 l') => refl_equal (D O (D 1 l')) | D _ _ => refl_equal _ @@ -461,7 +461,7 @@ one would expect that the compilation of G (this involves inversion) would produce: *) -Definition G (l:J O) : l = l := +Definition G (l:J O) : l = l := match l return l = l with | D 0 l'' => match l'' as _l'' in J n return @@ -480,3 +480,29 @@ Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) := | niln => w | consn a n' v' => consn _ a _ (app v' w) end. + +(* Testing regression of bug 2106 *) + +Set Implicit Arguments. +Require Import List. + +Inductive nt := E. +Definition root := E. +Inductive ctor : list nt -> nt -> Type := + Plus : ctor (cons E (cons E nil)) E. + +Inductive term : nt -> Type := +| Term : forall s n, ctor s n -> spine s -> term n +with spine : list nt -> Type := +| EmptySpine : spine nil +| ConsSpine : forall n s, term n -> spine s -> spine (n :: s). + +Inductive step : nt -> nt -> Type := + | Step : forall l n r n' (c:ctor (l++n::r) n'), spine l -> spine r -> step n +n'. + +Definition test (s:step E E) := + match s with + | Step nil _ (cons E nil) _ Plus l l' => true + | _ => false + end. |