diff options
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Cases.v | 71 | ||||
-rw-r--r-- | test-suite/success/CasesDep.v | 22 | ||||
-rw-r--r-- | test-suite/success/Hints.v | 5 | ||||
-rw-r--r-- | test-suite/success/Mod_params.v | 84 | ||||
-rw-r--r-- | test-suite/success/Notations.v | 14 | ||||
-rw-r--r-- | test-suite/success/RecTutorial.v | 69 | ||||
-rw-r--r-- | test-suite/success/Reset.v | 7 | ||||
-rw-r--r-- | test-suite/success/apply.v | 17 | ||||
-rw-r--r-- | test-suite/success/coercions.v | 42 | ||||
-rw-r--r-- | test-suite/success/dependentind.v | 31 | ||||
-rw-r--r-- | test-suite/success/evars.v | 70 | ||||
-rw-r--r-- | test-suite/success/hyps_inclusion.v | 8 | ||||
-rw-r--r-- | test-suite/success/telescope_canonical.v | 70 |
13 files changed, 359 insertions, 151 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 745529bf..f445ca8e 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -100,7 +100,7 @@ Type (fun x : nat => match x return nat with | x => x end). -Section testlist. +Module Type testlist. Parameter A : Set. Inductive list : Set := | nil : list @@ -119,7 +119,6 @@ Definition titi (a : A) (l : list) := | nil => l | cons b l => l end. -Reset list. End testlist. @@ -913,71 +912,77 @@ Type | LeS n m _ => (S n, S m) end). - +Module Type F_v1. Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := match h in (Le n m) return (Le n (S m)) with | LeO m' => LeO (S m') | LeS n' m' h' => LeS n' (S m') (F n' m' h') end. +End F_v1. -Reset F. - +Module Type F_v2. Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := match h in (Le n m) return (Le n (S m)) with | LeS n m h => LeS n (S m) (F n m h) | LeO m => LeO (S m) end. +End F_v2. (* Rend la longueur de la liste *) -Definition length1 (n : nat) (l : listn n) := + +Module Type L1. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => 1 | _ => 0 end. +End L1. -Reset length1. -Definition length1 (n : nat) (l : listn n) := +Module Type L1'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => 1 | _ => 0 end. +End L1'. - -Definition length2 (n : nat) (l : listn n) := +Module Type L2. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => S n | _ => 0 end. +End L2. -Reset length2. - -Definition length2 (n : nat) (l : listn n) := +Module Type L2'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => S n | _ => 0 end. +End L2'. -Definition length3 (n : nat) (l : listn n) := +Module Type L3. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ l) => S n | consn n _ _ => 1 | _ => 0 end. +End L3. - -Reset length3. - -Definition length3 (n : nat) (l : listn n) := +Module Type L3'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ l) => S n | consn n _ _ => 1 | _ => 0 end. - +End L3'. Type match LeO 0 return nat with | LeS n m h => n + m @@ -1256,7 +1261,7 @@ Type match (0, 0) with | (x, y) => (S x, S y) end. - +Module Type test_concat. Parameter concat : forall A : Set, List A -> List A -> List A. @@ -1273,6 +1278,7 @@ Type | _, _ => Nil nat end. +End test_concat. Inductive redexes : Set := | VAR : nat -> redexes @@ -1295,7 +1301,6 @@ Type (fun n : nat => match n with | _ => 0 end). -Reset concat. Parameter concat : forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m). @@ -1383,6 +1388,7 @@ Type (* I.e. to test manipulation of elimination predicate *) (* ===================================================================== *) +Module Type test_term. Parameter LTERM : nat -> Set. Inductive TERM : Type := @@ -1397,7 +1403,8 @@ Type | oper op1 l1, oper op2 l2 => False | _, _ => False end. -Reset LTERM. + +End test_term. @@ -1493,6 +1500,7 @@ Type end. +Module Type ff. Parameter ff : forall n m : nat, n <> m -> S n <> S m. Parameter discr_r : forall n : nat, 0 <> S n. @@ -1505,6 +1513,7 @@ Type | S x => or_intror (S x = 0) (discr_l x) end). +Module Type eqdec. Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := match n, m return (n = m \/ n <> m) with @@ -1518,7 +1527,9 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := end end. -Reset eqdec. +End eqdec. + +Module Type eqdec'. Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := match n return (forall m : nat, n = m \/ n <> m) with @@ -1540,6 +1551,7 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := end end. +End eqdec'. Inductive empty : forall n : nat, listn n -> Prop := intro_empty : empty 0 niln. @@ -1554,7 +1566,10 @@ Type | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y) end). -Reset ff. +End ff. + +Module Type ff'. + Parameter ff : forall n m : nat, n <> m -> S n <> S m. Parameter discr_r : forall n : nat, 0 <> S n. Parameter discr_l : forall n : nat, S n <> 0. @@ -1566,6 +1581,7 @@ Type | S x => or_intror (S x = 0) (discr_l x) end). +Module Type eqdec. Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := match n, m return (n = m \/ n <> m) with @@ -1578,7 +1594,10 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := | or_intror h => or_intror (S x = S y) (ff x y h) end end. -Reset eqdec. + +End eqdec. + +Module Type eqdec'. Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := match n return (forall m : nat, n = m \/ n <> m) with @@ -1600,6 +1619,8 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := end end. +End eqdec'. +End ff'. (* ================================================== *) (* Pour tester parametres *) diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index d3b7cf3f..bfead53c 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -222,7 +222,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci. de l'arite de chaque operateur *) -Section Sig. +Module Sig. Record Signature : Type := {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}. @@ -277,7 +277,7 @@ Type | _, _ => False end. - +Module Type Version1. Definition equalT (t1 t2 : TERM) : Prop := match t1, t2 with @@ -294,12 +294,15 @@ Definition EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) | _, _ => False end. +End Version1. + -Reset equalT. (* ------------------------------------------------------------------*) (* Initial exemple (without patterns) *) (*-------------------------------------------------------------------*) +Module Version2. + Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 return (TERM -> Prop) with | var v1 => @@ -347,11 +350,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version2. (* ---------------------------------------------------------------- *) (* Version with simple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version3. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -388,8 +393,9 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version3. -Reset equalT. +Module Version4. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -423,10 +429,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version4. + (* ---------------------------------------------------------------- *) (* Version with multiple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version5. Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := match t1, t2 with @@ -445,6 +454,7 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := | _, _ => False end. +End Version5. (* ------------------------------------------------------------------ *) diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index a93f8900..071fb957 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -16,11 +16,6 @@ Hint Immediate refl_equal sym_equal: foo. Hint Unfold fst sym_equal. Hint Unfold fst sym_equal: foo. -(* What's this stranged syntax ? *) -Hint Destruct h6 := 4 Conclusion (_ <= _) => fun H => apply H. -Hint Destruct h7 := 4 Discardable Hypothesis (_ <= _) => fun H => apply H. -Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H. - (* Checks that local names are accepted *) Section A. Remark Refl : forall (A : Set) (x : A), x = x. diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v index 74228bbb..51516166 100644 --- a/test-suite/success/Mod_params.v +++ b/test-suite/success/Mod_params.v @@ -20,59 +20,31 @@ End Q. #trace Nametab.exists_cci;; *) -Module M. -Reset M. -Module M (X: SIG). -Reset M. -Module M (X Y: SIG). -Reset M. -Module M (X: SIG) (Y: SIG). -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG). -Reset M. -Module M (X: SIG) (Y: SIG). -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG). -Reset M. -Module M : SIG. -Reset M. -Module M (X: SIG) : SIG. -Reset M. -Module M (X Y: SIG) : SIG. -Reset M. -Module M (X: SIG) (Y: SIG) : SIG. -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG) : SIG. -Reset M. -Module M (X: SIG) (Y: SIG) : SIG. -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG) : SIG. -Reset M. -Module M := F Q. -Reset M. -Module M (X: FSIG) := X Q. -Reset M. -Module M (X Y: FSIG) := X Q. -Reset M. -Module M (X: FSIG) (Y: SIG) := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) := X Z. -Reset M. -Module M (X: FSIG) (Y: SIG) := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) := X Z. -Reset M. -Module M : SIG := F Q. -Reset M. -Module M (X: FSIG) : SIG := X Q. -Reset M. -Module M (X Y: FSIG) : SIG := X Q. -Reset M. -Module M (X: FSIG) (Y: SIG) : SIG := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. -Reset M. -Module M (X: FSIG) (Y: SIG) : SIG := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. -Reset M. +Module M01. End M01. +Module M02 (X: SIG). End M02. +Module M03 (X Y: SIG). End M03. +Module M04 (X: SIG) (Y: SIG). End M04. +Module M05 (X Y: SIG) (Z1 Z: SIG). End M05. +Module M06 (X: SIG) (Y: SIG). End M06. +Module M07 (X Y: SIG) (Z1 Z: SIG). End M07. +Module M08 : SIG. End M08. +Module M09 (X: SIG) : SIG. End M09. +Module M10 (X Y: SIG) : SIG. End M10. +Module M11 (X: SIG) (Y: SIG) : SIG. End M11. +Module M12 (X Y: SIG) (Z1 Z: SIG) : SIG. End M12. +Module M13 (X: SIG) (Y: SIG) : SIG. End M13. +Module M14 (X Y: SIG) (Z1 Z: SIG) : SIG. End M14. +Module M15 := F Q. +Module M16 (X: FSIG) := X Q. +Module M17 (X Y: FSIG) := X Q. +Module M18 (X: FSIG) (Y: SIG) := X Y. +Module M19 (X Y: FSIG) (Z1 Z: SIG) := X Z. +Module M20 (X: FSIG) (Y: SIG) := X Y. +Module M21 (X Y: FSIG) (Z1 Z: SIG) := X Z. +Module M22 : SIG := F Q. +Module M23 (X: FSIG) : SIG := X Q. +Module M24 (X Y: FSIG) : SIG := X Q. +Module M25 (X: FSIG) (Y: SIG) : SIG := X Y. +Module M26 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. +Module M27 (X: FSIG) (Y: SIG) : SIG := X Y. +Module M28 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index f5f5a9d1..89f11059 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -17,10 +17,12 @@ Check (nat |= nat --> nat). (* Check that first non empty definition at an empty level can be of any associativity *) -Definition marker := O. +Module Type v1. Notation "x +1" := (S x) (at level 8, left associativity). -Reset marker. +End v1. +Module Type v2. Notation "x +1" := (S x) (at level 8, right associativity). +End v2. (* Check that empty levels (here 8 and 2 in pattern) are added in the right order *) @@ -86,3 +88,11 @@ Notation "'FOO' x" := (S x) (at level 40). Goal (2 ++++ 3) = 5. reflexivity. Abort. + +(* Check correct failure handling when a non-constructor notation is + used in cases pattern (bug #2724 in 8.3 and 8.4beta) *) + +Notation "'FORALL' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +Fail Check fun x => match x with S (FORALL x, _) => 0 end. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 2602c7e3..64048fe2 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -1,3 +1,5 @@ +Module Type LocalNat. + Inductive nat : Set := | O : nat | S : nat->nat. @@ -5,7 +7,8 @@ Check nat. Check O. Check S. -Reset nat. +End LocalNat. + Print nat. @@ -477,10 +480,10 @@ Qed. -(* -Check (fun (P:Prop->Prop)(p: ex_Prop P) => +Fail Check (fun (P:Prop->Prop)(p: ex_Prop P) => match p with exP_intro X HX => X end). +(* Error: Incorrect elimination of "p" in the inductive type "ex_Prop", the return type has sort "Type" while it should be @@ -489,12 +492,11 @@ Incorrect elimination of "p" in the inductive type Elimination of an inductive object of sort "Prop" is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs - *) -(* -Check (match prop_inject with (prop_intro P p) => P end). +Fail Check (match prop_inject with (prop_intro p) => p end). +(* Error: Incorrect elimination of "prop_inject" in the inductive type "prop", the return type has sort "Type" while it should be @@ -503,13 +505,12 @@ Incorrect elimination of "prop_inject" in the inductive type Elimination of an inductive object of sort "Prop" is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs - *) Print prop_inject. (* prop_inject = -prop_inject = prop_intro prop (fun H : prop => H) +prop_inject = prop_intro prop : prop *) @@ -520,26 +521,24 @@ Inductive typ : Type := Definition typ_inject: typ. split. exact typ. +Fail Defined. (* -Defined. - Error: Universe Inconsistency. *) Abort. -(* -Inductive aSet : Set := +Fail Inductive aSet : Set := aSet_intro: Set -> aSet. - - +(* User error: Large non-propositional inductive types must be in Type - *) Inductive ex_Set (P : Set -> Prop) : Type := exS_intro : forall X : Set, P X -> ex_Set P. +Module Type Version1. + Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop := c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p). @@ -553,21 +552,15 @@ Goal ~(comes_from_the_left _ _ (or_intror True I)). *) Abort. -Reset comes_from_the_left. - -(* +End Version1. - - - - - - Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop := +Fail Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop := match H with | or_introl p => True | or_intror q => False end. +(* Error: Incorrect elimination of "H" in the inductive type "or", the return type has sort "Type" while it should be @@ -576,7 +569,6 @@ Incorrect elimination of "H" in the inductive type Elimination of an inductive object of sort "Prop" is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs - *) Definition comes_from_the_left_sumbool @@ -737,6 +729,7 @@ Fixpoint plus'' (n p:nat) {struct n} : nat := | S m => plus'' m (S p) end. +Module Type even_test_v1. Fixpoint even_test (n:nat) : bool := match n @@ -745,8 +738,9 @@ Fixpoint even_test (n:nat) : bool := | S (S p) => even_test p end. +End even_test_v1. -Reset even_test. +Module even_test_v2. Fixpoint even_test (n:nat) : bool := match n @@ -761,12 +755,8 @@ with odd_test (n:nat) : bool := | S p => even_test p end. - - Eval simpl in even_test. - - Eval simpl in (fun x : nat => even_test x). Eval simpl in (fun x : nat => plus 5 x). @@ -774,6 +764,8 @@ Eval simpl in (fun x : nat => even_test (plus 5 x)). Eval simpl in (fun x : nat => even_test (plus x 5)). +End even_test_v2. + Section Principle_of_Induction. Variable P : nat -> Prop. @@ -866,14 +858,13 @@ Print Acc. Require Import Minus. -(* -Fixpoint div (x y:nat){struct x}: nat := +Fail Fixpoint div (x y:nat){struct x}: nat := if eq_nat_dec x 0 then 0 else if eq_nat_dec y 0 then x else S (div (x-y) y). - +(* Error: Recursive definition of div is ill-formed. In environment @@ -971,19 +962,15 @@ Proof. intros A v;inversion v. Abort. -(* - Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), - n= 0 -> v = Vnil A. -Toplevel input, characters 40281-40287 -> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vnil A. -> ^^^^^^ +Fail Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), + n= 0 -> v = Vector.nil A. +(* Error: In environment A : Set n : nat v : Vector.t A n -e : n = 0 -The term "Vnil A" has type "Vector.t A 0" while it is expected to have type +The term "[]" has type "Vector.t A 0" while it is expected to have type "Vector.t A n" *) Require Import JMeq. diff --git a/test-suite/success/Reset.v b/test-suite/success/Reset.v deleted file mode 100644 index b71ea69d..00000000 --- a/test-suite/success/Reset.v +++ /dev/null @@ -1,7 +0,0 @@ -(* Check Reset Section *) - -Section A. -Definition B := Prop. -End A. - -Reset A. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index e3183ef2..d3c76101 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -97,13 +97,14 @@ Qed. (* Check use of unification of bindings types in specialize *) +Module Type Test. Variable P : nat -> Prop. Variable L : forall (l : nat), P l -> P l. Goal P 0 -> True. intros. specialize L with (1:=H). Abort. -Reset P. +End Test. (* Two examples that show that hnf_constr is used when unifying types of bindings (a simplification of a script from Field_Theory) *) @@ -415,3 +416,17 @@ apply mapfuncomp. Abort. End A. + +(* Check "with" clauses refer to names as they are printed *) + +Definition hide p := forall n:nat, p = n. + +Goal forall n, (forall n, n=0) -> hide n -> n=0. +unfold hide. +intros n H H'. +(* H is displayed as (forall n, n=0) *) +apply H with (n:=n). +Undo. +(* H' is displayed as (forall n0, n=n0) *) +apply H' with (n0:=0). +Qed. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 001beae7..4292ecb6 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -89,3 +89,45 @@ Module A. End A. Import A. Fail Check S true. + +(* Tests after the inheritance condition constraint is relaxed *) + +Inductive list (A : Type) : Type := + nil : list A | cons : A -> list A -> list A. +Inductive vect (A : Type) : nat -> Type := + vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n). +Fixpoint size A (l : list A) : nat := match l with nil => 0 | cons _ tl => 1+size _ tl end. + +Section test_non_unif_but_complete. +Fixpoint l2v A (l : list A) : vect A (size A l) := + match l as l return vect A (size A l) with + | nil => vnil A + | cons x xs => vcons A (size A xs) x (l2v A xs) + end. + +Local Coercion l2v : list >-> vect. +Check (fun l : list nat => (l : vect _ _)). + +End test_non_unif_but_complete. + +Section what_we_could_do. +Variables T1 T2 : Type. +Variable c12 : T1 -> T2. + +Class coercion (A B : Type) : Type := cast : A -> B. +Instance atom : coercion T1 T2 := c12. +Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) (B * D) := + fun x => (c1 (fst x), c2 (snd x)). + +Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) := + match l as l return vect B (size A l) with + | nil => vnil B + | cons x xs => vcons _ _ (c x) (l2v2 xs) end. + +Local Coercion l2v2 : list >-> vect. + +(* This shows that there is still something to do to take full profit + of coercions *) +Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). +Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). +Section what_we_could_do.
\ No newline at end of file diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index fe0165d0..79d12a06 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,5 +1,11 @@ Require Import Coq.Program.Program Coq.Program.Equality. +Goal forall (H: forall n m : nat, n = m -> n = 0) x, x = tt. +intros. +dependent destruction x. +reflexivity. +Qed. + Variable A : Set. Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n). @@ -84,6 +90,29 @@ Proof with simpl in * ; eqns ; eauto with lambda. intro. eapply app... Defined. +Lemma weakening_ctx : forall Γ Δ τ, Γ ; Δ ⊢ τ -> + forall Δ', Γ ; Δ' ; Δ ⊢ τ. +Proof with simpl in * ; eqns ; eauto with lambda. + intros Γ Δ τ H. + + dependent induction H. + + destruct Δ as [|Δ τ'']... + induction Δ'... + + destruct Δ as [|Δ τ'']... + induction Δ'... + + destruct Δ as [|Δ τ'']... + apply abs. + specialize (IHterm Γ (empty, τ))... + + apply abs. + specialize (IHterm Γ (Δ, τ'', τ))... + + intro. eapply app... +Defined. + Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; eqns ; eauto. intros until 1. @@ -105,6 +134,8 @@ Proof with simpl in * ; eqns ; eauto. eapply app... Defined. + + (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) Set Implicit Arguments. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 2f1ec757..e6088091 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -309,3 +309,73 @@ Definition k6 Definition k7 (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat) (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b). + +(* An example that uses materialize_evar under binders *) +(* Extracted from bigop.v in the mathematical components library *) + +Section Bigop. + +Variable bigop : forall R I: Type, + R -> (R -> R -> R) -> list I -> (I->Prop) -> (I -> R) -> R. + +Hypothesis eq_bigr : +forall (R : Type) (idx : R) (op : R -> R -> R) + (I : Type) (r : list I) (P : I -> Prop) (F1 F2 : I -> R), + (forall i : I, P i -> F1 i = F2 i) -> + bigop R I idx op r (fun i : I => P i) (fun i : I => F1 i) = idx. + +Hypothesis big_tnth : +forall (R : Type) (idx : R) (op : R -> R -> R) + (I : Type) (r : list I) (P : I -> Prop) (F : I -> R), + bigop R I idx op r (fun i : I => P i) (fun i : I => F i) = idx. + +Hypothesis big_tnth_with_letin : +forall (R : Type) (idx : R) (op : R -> R -> R) + (I : Type) (r : list I) (P : I -> Prop) (F : I -> R), + bigop R I idx op r (fun i : I => let i:=i in P i) (fun i : I => F i) = idx. + +Variable R : Type. +Variable idx : R. +Variable op : R -> R -> R. +Variable I : Type. +Variable J : Type. +Variable rI : list I. +Variable rJ : list J. +Variable xQ : J -> Prop. +Variable P : I -> Prop. +Variable Q : I -> J -> Prop. +Variable F : I -> J -> R. + +(* Check unification under binders *) + +Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth _ _ _ _ rI _ _)) + : (bigop R J idx op rJ + (fun j : J => let k:=j in xQ k) + (fun j : J => let k:=j in + bigop R I idx + op rI + (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx. + +(* Check also with let-in *) + +Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _)) + : (bigop R J idx op rJ + (fun j : J => let k:=j in xQ k) + (fun j : J => let k:=j in + bigop R I idx + op rI + (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx. + +End Bigop. + +(* Check the use of (at least) an heuristic to solve problems of the form + "?x[t] = ?y" where ?y occurs in t without easily knowing if ?y can + eventually be erased in t *) + +Section evar_evar_occur. + Variable id : nat -> nat. + Variable f : forall x, id x = 0 -> id x = 0 -> x = 1 /\ x = 2. + Variable g : forall y, id y = 0 /\ id y = 0. + (* Still evars in the resulting type, but constraints should be solved *) + Check match g _ with conj a b => f _ a b end. +End evar_evar_occur. diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v index af81e53d..ebd90a40 100644 --- a/test-suite/success/hyps_inclusion.v +++ b/test-suite/success/hyps_inclusion.v @@ -19,14 +19,16 @@ red in H. (* next tactic was failing wrt bug #1325 because type-checking the goal detected a syntactically different type for the section variable H *) case 0. -Reset A. +Abort. +End A. (* Variant with polymorphic inductive types for bug #1325 *) -Section A. +Section B. Variable H:not True. Inductive I (n:nat) : Type := C : H=H -> I n. Goal I 0. red in H. case 0. -Reset A. +Abort. +End B. diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v index 8a607c93..73df5ca9 100644 --- a/test-suite/success/telescope_canonical.v +++ b/test-suite/success/telescope_canonical.v @@ -1,12 +1,72 @@ Structure Inner := mkI { is :> Type }. Structure Outer := mkO { os :> Inner }. - Canonical Structure natInner := mkI nat. Canonical Structure natOuter := mkO natInner. - Definition hidden_nat := nat. - Axiom P : forall S : Outer, is (os S) -> Prop. - -Lemma foo (n : hidden_nat) : P _ n. +Lemma test1 (n : hidden_nat) : P _ n. Admitted. + +Structure Pnat := mkP { getp : nat }. +Definition my_getp := getp. +Axiom W : nat -> Prop. + +(* Fix *) +Canonical Structure add1Pnat n := mkP (plus n 1). +Definition test_fix n := (refl_equal _ : W (my_getp _) = W (n + 1)). + +(* Case *) +Definition pred n := match n with 0 => 0 | S m => m end. +Canonical Structure predSS n := mkP (pred n). +Definition test_case x := (refl_equal _ : W (my_getp _) = W (pred x)). +Fail Definition test_case' := (refl_equal _ : W (my_getp _) = W (pred 0)). + +Canonical Structure letPnat' := mkP 0. +Definition letin := (let n := 0 in n). +Definition test4 := (refl_equal _ : W (getp _) = W letin). +Definition test41 := (refl_equal _ : W (my_getp _) = W letin). +Definition letin2 (x : nat) := (let n := x in n). +Canonical Structure letPnat'' x := mkP (letin2 x). +Definition test42 x := (refl_equal _ : W (my_getp _) = W (letin2 x)). +Fail Definition test42' x := (refl_equal _ : W (my_getp _) = W x). + +Structure Morph := mkM { f :> nat -> nat }. +Definition my_f := f. +Axiom Q : (nat -> nat) -> Prop. + +(* Lambda *) +Canonical Structure addMorh x := mkM (plus x). +Definition test_lam x := (refl_equal _ : Q (my_f _) = Q (plus x)). +Definition test_lam' := (refl_equal _ : Q (my_f _) = Q (plus 0)). + +(* Simple tests to justify Sort and Prod as "named". + They are already normal, so they cannot loose their names, + but still... *) +Structure Sot := mkS { T : Type }. +Axiom R : Type -> Prop. +Canonical Structure tsot := mkS (Type). +Definition test_sort := (refl_equal _ : R (T _) = R Type). +Canonical Structure tsot2 := mkS (nat -> nat). +Definition test_prod := (refl_equal _ : R (T _) = R (nat -> nat)). + +(* Var *) +Section Foo. +Variable v : nat. +Definition my_v := v. +Canonical Structure vP := mkP my_v. +Definition test_var := (refl_equal _ : W (getp _) = W my_v). +Canonical Structure vP' := mkP v. +Definition test_var' := (refl_equal _ : W (my_getp _) = W my_v). +End Foo. + +(* Rel *) +Definition test_rel v := (refl_equal _ : W (my_getp _) = W (my_v v)). +Goal True. +pose (x := test_rel 2). +match goal with x := _ : W (my_getp (vP 2)) = _ |- _ => idtac end. +apply I. +Qed. + + + + |