diff options
Diffstat (limited to 'test-suite/bugs/closed')
95 files changed, 4769 insertions, 42 deletions
diff --git a/test-suite/bugs/closed/1784.v b/test-suite/bugs/closed/1784.v index 0b63d7b56..25d1b192e 100644 --- a/test-suite/bugs/closed/1784.v +++ b/test-suite/bugs/closed/1784.v @@ -91,9 +91,8 @@ Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H; subst. Defined. Next Obligation. intro H1; contradict H. inversion H1; subst. assumption. - contradict H0; assumption. Defined. -Next Obligation. - intro H1; contradict H0. inversion H1; subst. assumption. Defined. + contradict H0; assumption. Defined. +Next Obligation. intro H1; contradict H0. inversion H1; subst. assumption. Defined. Next Obligation. intro H1; contradict H. inversion H1; subst. assumption. Defined. Next Obligation. diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v index 0be859edd..7fae32871 100644 --- a/test-suite/bugs/closed/2310.v +++ b/test-suite/bugs/closed/2310.v @@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either leave P as subgoal or choose itself one solution *) -intros. refine (Cons (cast H _ y)).
\ No newline at end of file + intros. Fail refine (Cons (cast H _ y)). + Unset Solve Unification Constraints. (* Keep the unification constraint around *) + refine (Cons (cast H _ y)). + intros. + refine (Nest (prod X X)). Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/2839.v b/test-suite/bugs/closed/2839.v index e396fe06e..e727e2606 100644 --- a/test-suite/bugs/closed/2839.v +++ b/test-suite/bugs/closed/2839.v @@ -5,6 +5,6 @@ intro. Fail let H := match goal with - | [ H : appcontext G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' + | [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' end in pose H. diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v index ef110ad0d..5f80013df 100644 --- a/test-suite/bugs/closed/3045.v +++ b/test-suite/bugs/closed/3045.v @@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) := Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' }. -Arguments Compose {obj} [C s d d'] m1 m2 : rename. +Arguments Compose {obj} [C s d d'] _ _ : rename. Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. diff --git a/test-suite/bugs/closed/3070.v b/test-suite/bugs/closed/3070.v new file mode 100644 index 000000000..7a8feca58 --- /dev/null +++ b/test-suite/bugs/closed/3070.v @@ -0,0 +1,6 @@ +(* Testing subst wrt chains of dependencies *) + +Lemma foo (a1 a2 : Set) (b1 : a1 -> Prop) + (Ha : a1 = a2) (c : a1) (d : b1 c) : True. +Proof. + subst. diff --git a/test-suite/bugs/closed/3209.v b/test-suite/bugs/closed/3209.v new file mode 100644 index 000000000..855058b01 --- /dev/null +++ b/test-suite/bugs/closed/3209.v @@ -0,0 +1,75 @@ +(* Avoiding some occur-check *) + +(* 1. Original example *) + +Inductive eqT {A} (x : A) : A -> Type := + reflT : eqT x x. +Definition Bi_inv (A B : Type) (f : (A -> B)) := + sigT (fun (g : B -> A) => + sigT (fun (h : B -> A) => + sigT (fun (α : forall b : B, eqT (f (g b)) b) => + forall a : A, eqT (h (f a)) a))). +Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f). + +Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B). +Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B := + sigT_rect (fun _ => TEquiv A B) + (fun (f : TEquiv A B -> eqT A B) H => + sigT_rect _ (* (fun _ => TEquiv A B) *) + (fun g _ => g e) + H) + (UA A B). + +(* 2. Alternative example by Guillaume *) + +Inductive foo (A : Prop) : Prop := Foo : foo A. +Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop. + +(* This used to fail with a Not_found, we fail more graciously but a + heuristic could be implemented, e.g. in some smart occur-check + function, to find a solution of then form ?P := fun _ => ?P' *) + +Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)). + +(* This works and tells which solution we could have inferred *) + +Check (fun e : ?[T] => bar ?[A] (fun _ => ?[P]) (fun g : ?[A'] => g e)). + +(* For the record, here is the trace in the failing example: + +In (fun e : ?T => bar ?[A] ?[P] (fun g : ?A' => g e)), we have the existential variables + +e:?T |- ?A : Prop +e:?T |- ?P : foo ?A -> Prop +e:?T |- ?A' : Type + +with constraints + +?A' == ?A +?A' == ?T -> ?P (Foo ?A) + +To type (g e), unification first defines + +?A := forall x:?B, ?P'{e:=e,x:=x} +with ?T <= ?B +and ?P'@{e:=e,x:=e} <= ?P@{e:=e} (Foo (forall x:?B, ?P'{e:=e,x:=x})) + +Then, since ?P'@{e:=e,x:=e} may use "e" in two different ways, it is +not a pattern and we define a new + +e:?T x:?B|- ?P'' : foo (?B' -> ?P''') -> Prop + +for some ?B' and ?P''', together with + +?P'@{e,x} := ?P''{e:=e,x:=e} (Foo (?B -> ?P') +?P@{e} := ?P''{e:=e,x:=e} + +Moreover, ?B' and ?P''' have to satisfy + +?B'@{e:=e,x:=e} == ?B@{e:=e} +?P'''@{e:=e,x:=e} == ?P'@{e:=e,x:=x} + +and this leads to define ?P' which was the initial existential +variable to define. +*) + diff --git a/test-suite/bugs/closed/3251.v b/test-suite/bugs/closed/3251.v index 5a7ae2002..d4ce050c5 100644 --- a/test-suite/bugs/closed/3251.v +++ b/test-suite/bugs/closed/3251.v @@ -1,4 +1,5 @@ Goal True. +idtac. Ltac foo := idtac. (* print out happens twice: foo is defined diff --git a/test-suite/bugs/closed/3383.v b/test-suite/bugs/closed/3383.v new file mode 100644 index 000000000..25257644a --- /dev/null +++ b/test-suite/bugs/closed/3383.v @@ -0,0 +1,6 @@ +Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end. +intro. +lazymatch goal with +| [ |- context[match ?b as b' in bool return @?P b' with true => ?t | false => ?f end] ] + => change (match b as b' in bool return P b' with true => t | false => f end) with (@bool_rect P t f b) +end. diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v index f9b2c3861..ee8cabf17 100644 --- a/test-suite/bugs/closed/3424.v +++ b/test-suite/bugs/closed/3424.v @@ -13,6 +13,7 @@ Notation "0" := (trunc_S minus_one) : trunc_scope. Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Notation IsHProp := (IsTrunc minus_one). Notation IsHSet := (IsTrunc 0). +Set Refolding Reduction. Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. Proof. intros. diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v new file mode 100644 index 000000000..50d297807 --- /dev/null +++ b/test-suite/bugs/closed/3441.v @@ -0,0 +1,23 @@ +Axiom f : nat -> nat -> nat. +Fixpoint do_n (n : nat) (k : nat) := + match n with + | 0 => k + | S n' => do_n n' (f k k) + end. + +Notation big := (_ = _). +Axiom k : nat. +Goal True. +Timeout 1 let H := fresh "H" in + let x := constr:(let n := 17 in do_n n = do_n n) in + let y := (eval lazy in x) in + pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) +Timeout 1 let H := fresh "H" in + let x := constr:(let n := 17 in do_n n = do_n n) in + let y := (eval lazy in x) in + pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) + +Timeout 1 Time let H := fresh "H" in + let x := constr:(let n := 17 in do_n n = do_n n) in + let y := (eval lazy in x) in + assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v new file mode 100644 index 000000000..102a2aba0 --- /dev/null +++ b/test-suite/bugs/closed/3495.v @@ -0,0 +1,18 @@ +Require Import RelationClasses. + +Axiom R : Prop -> Prop -> Prop. +Declare Instance : Reflexive R. + +Class bar := { x : False }. +Record foo := { a : Prop ; b : bar }. + +Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}. + +Goal exists k, R k True. +Proof. +eexists. +evar (b : bar). +let e := match goal with |- R ?e _ => constr:(e) end in +unify e (a (default_foo True)). +subst b. +reflexivity. diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index fcdfa0057..9ed0926a6 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -1,4 +1,3 @@ -Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *) Require Coq.Setoids.Setoid. Import Coq.Setoids.Setoid. @@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops. Local Existing Instance ILFun_ILogic. Definition catOP (P Q: OPred) : OPred := admit. Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m. -admit. +apply admit. Defined. Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit. Class IsPointed (T : Type) := point : T. @@ -69,8 +68,27 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) pose P; refine (P _ _) end; unfold Basics.flip. - 2: solve [ apply reflexivity ]. - Undo. - 2: reflexivity. (* Toplevel input, characters 18-29: -Error: -Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file + Focus 2. + Set Typeclasses Debug. + Set Typeclasses Legacy Resolution. + apply reflexivity. + (* Debug: 1.1: apply @IsPointed_catOP on +(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) +Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) +Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) +Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) +Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities +Debug: Backtracking after apply @Equivalence_Reflexive +Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) +Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) +Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) +*) + Undo. Unset Typeclasses Legacy Resolution. + Test Typeclasses Unique Solutions. + Test Typeclasses Unique Instances. + Show Existentials. + Set Typeclasses Debug Verbosity 2. + Set Printing All. + (* As in 8.5, allow a shelved subgoal to remain *) + apply reflexivity. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/3563.v b/test-suite/bugs/closed/3563.v index 679721667..961563ed4 100644 --- a/test-suite/bugs/closed/3563.v +++ b/test-suite/bugs/closed/3563.v @@ -16,11 +16,11 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0) transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] => set(foo:=h); idtac end. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ] + | [ |- context ctx [transport (fun y => (?g (fst (y H2))))] ] => idtac end. Abort. @@ -30,7 +30,7 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0) transport (fun y : H1 -> (H1 -> H) * H0 => H5 (fst (y H2) H2)) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] => set(foo:=X) end. (* Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v index 495e67e09..f5a22bd50 100644 --- a/test-suite/bugs/closed/3647.v +++ b/test-suite/bugs/closed/3647.v @@ -650,4 +650,5 @@ Goal forall (ptest : program) (cond : Condition) (value : bool) Grab Existential Variables. subst_body; simpl. - refine (all_behead (projT2 _)). + Fail refine (all_behead (projT2 _)). + Unset Solve Unification Constraints. refine (all_behead (projT2 _)). diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index c24173abf..fd9640b89 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -47,7 +47,7 @@ Type@{Top.21} -> Type@{Top.23} Top.23 < Top.22 *) *) Fail Check @qux@{Set Set}. -Fail Check @qux@{Set Set Set}. +Check @qux@{Type Type Type Type}. (* [qux] should only need two universes *) -Check @qux@{i j k}. (* Error: The command has not failed!, but I think this is suboptimal *) +Check @qux@{i j k l}. (* Error: The command has not failed!, but I think this is suboptimal *) Fail Check @qux@{i j}. diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 8dadc2419..efa432526 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +46,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. @@ -111,8 +109,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +121,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. diff --git a/test-suite/bugs/closed/3753.v b/test-suite/bugs/closed/3753.v new file mode 100644 index 000000000..5bfbee949 --- /dev/null +++ b/test-suite/bugs/closed/3753.v @@ -0,0 +1,4 @@ +Axiom foo : Type -> Type. +Axiom bar : forall (T : Type), T -> foo T. +Arguments bar A x : rename. +About bar.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v index e594b74b6..666c64631 100644 --- a/test-suite/bugs/closed/3825.v +++ b/test-suite/bugs/closed/3825.v @@ -14,3 +14,11 @@ Notation qux := (nat -> nat). Fail Check qux@{i}. +Axiom TruncType@{i} : nat -> Type@{i}. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (0)-Type. + +Check hProp. +Check hProp@{i}. + diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v new file mode 100644 index 000000000..2ac4abe54 --- /dev/null +++ b/test-suite/bugs/closed/3886.v @@ -0,0 +1,23 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). + +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) + := _ +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) + := _. +Obligations. +Axiom cheat : forall {A}, A. +Obligation 1 of doubleE. +apply cheat. +Qed. + +Obligation 1 of doubleO. +apply cheat. +Qed. + +Check doubleE.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v new file mode 100644 index 000000000..a4adb23cc --- /dev/null +++ b/test-suite/bugs/closed/3920.v @@ -0,0 +1,7 @@ +Require Import Setoid. +Axiom P : nat -> Prop. +Axiom P_or : forall x y, P (x + y) <-> P x \/ P y. +Lemma foo (H : P 3) : False. +eapply or_introl in H. +erewrite <- P_or in H. +(* Error: No such hypothesis: H *) diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 21b03ce54..61527764e 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -49,3 +49,56 @@ Lemma bar {A} n m (x : A) : skipn n (replicate m x) = replicate (m - n) x. Proof. intros. f_equal. (* 8.5: one goal, n = m - n *) +Abort. + +Variable F : nat -> Set. +Variable X : forall n, F (n + 1). + +Definition sequator{X Y: Set}{eq:X=Y}(x:X) : Y := eq_rec _ _ x _ eq. +Definition tequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq. +Polymorphic Definition pequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq. + +Goal {n:nat & F (S n)}. +eexists. +unshelve eapply (sequator (X _)). +f_equal. (*behaves*) +Undo 2. +unshelve eapply (pequator (X _)). +f_equal. (*behaves*) +Undo 2. +unshelve eapply (tequator (X _)). +f_equal. (*behaves now *) +Focus 2. exact 0. +simpl. +reflexivity. +Defined. + +(* Part 2: modulo casts introduced by refine due to reductions in goals *) + +Goal {n:nat & F (S n)}. +eexists. +(*misbehaves, although same goal as above*) +Set Printing All. +unshelve refine (sequator (X _)); revgoals. +2:exact 0. reflexivity. +Undo 3. +unshelve refine (pequator (X _)); revgoals. +f_equal. +Undo 2. +unshelve refine (tequator (X _)); revgoals. +f_equal. +Admitted. + +Goal @eq Set nat nat. +congruence. +Qed. + +Goal @eq Type nat nat. +congruence. +Qed. + +Variable T : Type. + +Goal @eq Type T T. +congruence. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v new file mode 100644 index 000000000..ffd33d381 --- /dev/null +++ b/test-suite/bugs/closed/4095.v @@ -0,0 +1,87 @@ +(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *) +(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *) +Require Import Coq.Setoids.Setoid. +Generalizable All Variables. +Axiom admit : forall {T}, T. +Ltac admit := apply admit. +Class Equiv (A : Type) := equiv : relation A. +Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv. +Class ILogicOps Frm := { lentails: relation Frm; + ltrue: Frm; + land: Frm -> Frm -> Frm; + lor: Frm -> Frm -> Frm }. +Infix "|--" := lentails (at level 79, no associativity). +Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. +Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. +Infix "-|-" := lequiv (at level 85, no associativity). +Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. +Section ILogic_Fun. + Context (T: Type) `{TType: type T}. + Context `{IL: ILogic Frm}. + Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. + Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. +End ILogic_Fun. +Implicit Arguments ILFunFrm [[ILOps] [e]]. +Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; + ltrue := True; + land P Q := P /\ Q; + lor P Q := P \/ Q |}. +Axiom Action : Set. +Definition Actions := list Action. +Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }. +Definition OPred := ILFunFrm Actions Prop. +Local Existing Instance ILFun_Ops. +Local Existing Instance ILFun_ILogic. +Definition catOP (P Q: OPred) : OPred := admit. +Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m. +admit. +Defined. +Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit. +Class IsPointed (T : Type) := point : T. +Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)). +Record PointedOPred := mkPointedOPred { + OPred_pred :> OPred; + OPred_inhabited: IsPointed_OPred OPred_pred + }. +Existing Instance OPred_inhabited. +Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred + := {| OPred_pred := O ; OPred_inhabited := _ |}. +Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit. +Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) + (tr : T -> T) (O2 : PointedOPred) (x : T) + (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0), + exists e1 e2, + catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2. + intros; do 2 esplit. + rewrite <- catOPA. + lazymatch goal with + | |- ?R (?f ?a ?b) (?f ?a' ?b') => + let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred) + (@Morphisms.respectful OPred (OPred -> OPred) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop)) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==> + @lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP + catOP_entails_m_Proper a a' H b b' H') in + pose P; + refine (P _ _) + end. + Undo. + Fail lazymatch goal with + | |- ?R (?f ?a ?b) (?f ?a' ?b') => + let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in + set(p:=P) + end. (* Toplevel input, characters 15-182: +Error: Cannot infer an instance of type +"PointedOPred" for the variable p in environment: +T : Type +O0 : T -> OPred +O1 : T -> PointedOPred +tr : T -> T +O2 : PointedOPred +x0 : T +H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4187.v b/test-suite/bugs/closed/4187.v new file mode 100644 index 000000000..b13ca36a3 --- /dev/null +++ b/test-suite/bugs/closed/4187.v @@ -0,0 +1,709 @@ +(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=4187 *) +(* File reduced by coq-bug-finder from original input, then from 715 lines to 696 lines *) +(* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0 + coqtop version 8.4pl5 (December 2014) *) +Set Asymmetric Patterns. +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.List. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Global Set Implicit Arguments. +Global Generalizable All Variables. +Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x then true else false. +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Module Export ADTSynthesis_DOT_Common_DOT_Wf. +Module Export ADTSynthesis. +Module Export Common. +Module Export Wf. + +Section wf. + Section wf_prod. + Context A B (RA : relation A) (RB : relation B). +Definition prod_relation : relation (A * B). +exact (fun ab a'b' => + RA (fst ab) (fst a'b') \/ (fst a'b' = fst ab /\ RB (snd ab) (snd a'b'))). +Defined. + + Fixpoint well_founded_prod_relation_helper + a b + (wf_A : Acc RA a) (wf_B : well_founded RB) {struct wf_A} + : Acc prod_relation (a, b) + := match wf_A with + | Acc_intro fa => (fix wf_B_rec b' (wf_B' : Acc RB b') : Acc prod_relation (a, b') + := Acc_intro + _ + (fun ab => + match ab as ab return prod_relation ab (a, b') -> Acc prod_relation ab with + | (a'', b'') => + fun pf => + match pf with + | or_introl pf' + => @well_founded_prod_relation_helper + _ _ + (fa _ pf') + wf_B + | or_intror (conj pfa pfb) + => match wf_B' with + | Acc_intro fb + => eq_rect + _ + (fun a'' => Acc prod_relation (a'', b'')) + (wf_B_rec _ (fb _ pfb)) + _ + pfa + end + end + end) + ) b (wf_B b) + end. + + Definition well_founded_prod_relation : well_founded RA -> well_founded RB -> well_founded prod_relation. + Proof. + intros wf_A wf_B [a b]; hnf in *. + apply well_founded_prod_relation_helper; auto. + Defined. + End wf_prod. + + Section wf_projT1. + Context A (B : A -> Type) (R : relation A). +Definition projT1_relation : relation (sigT B). +exact (fun ab a'b' => + R (projT1 ab) (projT1 a'b')). +Defined. + + Definition well_founded_projT1_relation : well_founded R -> well_founded projT1_relation. + Proof. + intros wf [a b]; hnf in *. + induction (wf a) as [a H IH]. + constructor. + intros y r. + specialize (IH _ r (projT2 y)). + destruct y. + exact IH. + Defined. + End wf_projT1. +End wf. + +Section Fix3. + Context A (B : A -> Type) (C : forall a, B a -> Type) (D : forall a b, C a b -> Type) + (R : A -> A -> Prop) (Rwf : well_founded R) + (P : forall a b c, D a b c -> Type) + (F : forall x : A, (forall y : A, R y x -> forall b c d, P y b c d) -> forall b c d, P x b c d). +Definition Fix3 a b c d : @P a b c d. +exact (@Fix { a : A & { b : B a & { c : C b & D c } } } + (fun x y => R (projT1 x) (projT1 y)) + (well_founded_projT1_relation Rwf) + (fun abcd => P (projT2 (projT2 (projT2 abcd)))) + (fun x f => @F (projT1 x) (fun y r b c d => f (existT _ y (existT _ b (existT _ c d))) r) _ _ _) + (existT _ a (existT _ b (existT _ c d)))). +Defined. +End Fix3. + +End Wf. + +End Common. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Common_DOT_Wf. + +Module Export ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export ADTSynthesis. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Setoids.Setoid. +Import Coq.Classes.Morphisms. + + + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Definition str_le `{StringLike Char} (s1 s2 : String) + := length s1 < length s2 \/ s1 =s s2. + Infix "≤s" := str_le (at level 70, right associativity). + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str) + }. + + Arguments StringLikeProperties Char {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export ADTSynthesis. +Module Export Parsers. +Module Export ContextFreeGrammar. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Export ADTSynthesis.Parsers.StringLike.Core. +Import ADTSynthesis.Common. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + Section parse. + Context {HSL : StringLike Char}. + Variable G : grammar. + + Inductive parse_of (str : String) : productions -> Type := + | ParseHead : forall pat pats, parse_of_production str pat + -> parse_of str (pat::pats) + | ParseTail : forall pat pats, parse_of str pats + -> parse_of str (pat::pats) + with parse_of_production (str : String) : production -> Type := + | ParseProductionNil : length str = 0 -> parse_of_production str nil + | ParseProductionCons : forall n pat pats, + parse_of_item (take n str) pat + -> parse_of_production (drop n str) pats + -> parse_of_production str (pat::pats) + with parse_of_item (str : String) : item -> Type := + | ParseTerminal : forall ch, str ~= [ ch ] -> parse_of_item str (Terminal ch) + | ParseNonTerminal : forall nt, parse_of str (Lookup G nt) + -> parse_of_item str (NonTerminal nt). + End parse. +End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End ContextFreeGrammar. + +Module Export BaseTypes. + +Section recursive_descent_parser. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> String.string -> bool; + remove_nonterminal : nonterminals_listT -> String.string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. +End recursive_descent_parser. + +End BaseTypes. +Import Coq.Lists.List. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' predata}. + + Inductive minimal_parse_of + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall str0 valid str, + length str = 0 + -> @minimal_parse_of_production str0 valid str nil + | MinParseProductionCons : forall str0 valid str n pat pats, + str ≤s str0 + -> @minimal_parse_of_item str0 valid (take n str) pat + -> @minimal_parse_of_production str0 valid (drop n str) pats + -> @minimal_parse_of_production str0 valid str (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall str0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item str0 valid str (Terminal ch) + | MinParseNonTerminal + : forall str0 valid str (nt : String.string), + @minimal_parse_of_nonterminal str0 valid str nt + -> @minimal_parse_of_item str0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid (nt : String.string) str, + length str < length str0 + -> is_valid_nonterminal initial_nonterminals_data nt + -> @minimal_parse_of str initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal str0 valid str nt + | MinParseNonTerminalStrEq + : forall str0 str valid nonterminal, + str =s str0 + -> is_valid_nonterminal initial_nonterminals_data nonterminal + -> is_valid_nonterminal valid nonterminal + -> @minimal_parse_of str0 (remove_nonterminal valid nonterminal) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal str0 valid str nonterminal. +End cfg. +Import ADTSynthesis.Common. + +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT. + + Definition split_list_completeT `{data : @parser_computational_predataT} + {str0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : str ≤s str0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In n split_list) + * (minimal_parse_of_item (G := G) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type). + + Class boolean_parser_completeness_dataT' `{data : boolean_parser_dataT} := + { split_string_for_production_complete + : forall str0 valid str (pf : str ≤s str0) nt, + is_valid_nonterminal initial_nonterminals_data nt + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT data str0 valid it its str pf (split_string_for_production it its str) + end)) + (Lookup G nt) }. +End general. + +Module Export BooleanRecognizer. +Import Coq.Numbers.Natural.Peano.NPeano. +Import Coq.Arith.Compare_dec. +Import Coq.Arith.Wf_nat. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}. + Context {data : @boolean_parser_dataT Char _}. + + Section bool. + Section parts. +Definition parse_item + (str_matches_nonterminal : String.string -> bool) + (str : String) + (it : item Char) + : bool. +Admitted. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : String), + str ≤s str0 + -> String.string + -> bool). + + Fixpoint parse_production + (str : String) + (pf : str ≤s str0) + (prod : production Char) + : bool. + Proof. + refine + match prod with + | nil => + + Nat.eq_dec (length str) 0 + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (map (fun n => + (parse_item + (parse_nonterminal (str := take n str) _) + (take n str) + it) + && parse_production' (drop n str) _)%bool + (split_string_for_production it its str)) + end; + revert pf; clear -HSLP; intros; admit. + Defined. + End production. + + Section productions. + Context {str0} + (parse_nonterminal + : forall (str : String) + (pf : str ≤s str0), + String.string -> bool). +Definition parse_productions + (str : String) + (pf : str ≤s str0) + (prods : productions Char) + : bool. +exact (fold_right orb + false + (map (parse_production parse_nonterminal pf) + prods)). +Defined. + End productions. + + Section nonterminals. + Section step. + Context {str0 valid} + (parse_nonterminal + : forall (p : String * nonterminals_listT), + prod_relation (ltof _ length) nonterminals_listT_R p (str0, valid) + -> forall str : String, + str ≤s fst p -> String.string -> bool). + + Definition parse_nonterminal_step + (str : String) + (pf : str ≤s str0) + (nt : String.string) + : bool. + Proof. + refine + (if lt_dec (length str) (length str0) + then + parse_productions + (@parse_nonterminal + (str : String, initial_nonterminals_data) + (or_introl _)) + (or_intror (reflexivity _)) + (Lookup G nt) + else + if Sumbool.sumbool_of_bool (is_valid_nonterminal valid nt) + then + parse_productions + (@parse_nonterminal + (str0 : String, remove_nonterminal valid nt) + (or_intror (conj eq_refl (remove_nonterminal_dec _ nt _)))) + (str := str) + _ + (Lookup G nt) + else + false); + assumption. + Defined. + End step. + + Section wf. +Definition parse_nonterminal_or_abort + : forall (p : String * nonterminals_listT) + (str : String), + str ≤s fst p + -> String.string + -> bool. +exact (Fix3 + _ _ _ + (well_founded_prod_relation + (well_founded_ltof _ length) + ntl_wf) + _ + (fun sl => @parse_nonterminal_step (fst sl) (snd sl))). +Defined. +Definition parse_nonterminal + (str : String) + (nt : String.string) + : bool. +exact (@parse_nonterminal_or_abort + (str : String, initial_nonterminals_data) str + (or_intror (reflexivity _)) nt). +Defined. + End wf. + End nonterminals. + End parts. + End bool. +End recursive_descent_parser. + +Section cfg. + Context {Char} {HSL : StringLike Char} {HSLP : @StringLikeProperties Char HSL} (G : grammar Char). + + Section definitions. + Context (P : String -> String.string -> Type). + + Definition Forall_parse_of_item' + (Forall_parse_of : forall {str pats} (p : parse_of G str pats), Type) + {str it} (p : parse_of_item G str it) + := match p return Type with + | ParseTerminal ch pf => unit + | ParseNonTerminal nt p' + => (P str nt * Forall_parse_of p')%type + end. + + Fixpoint Forall_parse_of {str pats} (p : parse_of G str pats) + := match p with + | ParseHead pat pats p' + => Forall_parse_of_production p' + | ParseTail _ _ p' + => Forall_parse_of p' + end + with Forall_parse_of_production {str pat} (p : parse_of_production G str pat) + := match p return Type with + | ParseProductionNil pf => unit + | ParseProductionCons pat strs pats p' p'' + => (Forall_parse_of_item' (@Forall_parse_of) p' * Forall_parse_of_production p'')%type + end. + + Definition Forall_parse_of_item {str it} (p : parse_of_item G str it) + := @Forall_parse_of_item' (@Forall_parse_of) str it p. + End definitions. + + End cfg. + +Section recursive_descent_parser_list. + Context {Char} {HSL : StringLike Char} {HLSP : StringLikeProperties Char} {G : grammar Char}. +Definition rdp_list_nonterminals_listT : Type. +exact (list String.string). +Defined. +Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> String.string -> bool. +admit. +Defined. +Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> String.string -> rdp_list_nonterminals_listT. +admit. +Defined. +Definition rdp_list_nonterminals_listT_R : rdp_list_nonterminals_listT -> rdp_list_nonterminals_listT -> Prop. +exact (ltof _ (@List.length _)). +Defined. + Lemma rdp_list_remove_nonterminal_dec : forall ls prods, + @rdp_list_is_valid_nonterminal ls prods = true + -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls. +admit. +Defined. + Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R. + Proof. + unfold rdp_list_nonterminals_listT_R. + intro. + apply well_founded_ltof. + Defined. + + Global Instance rdp_list_predata : parser_computational_predataT + := { nonterminals_listT := rdp_list_nonterminals_listT; + initial_nonterminals_data := Valid_nonterminals G; + is_valid_nonterminal := rdp_list_is_valid_nonterminal; + remove_nonterminal := rdp_list_remove_nonterminal; + nonterminals_listT_R := rdp_list_nonterminals_listT_R; + remove_nonterminal_dec := rdp_list_remove_nonterminal_dec; + ntl_wf := rdp_list_ntl_wf }. +End recursive_descent_parser_list. + +Section sound. + Section general. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' predata}. + + Section parts. + + Section nonterminals. + Section wf. + + Lemma parse_nonterminal_sound + (str : String) (nonterminal : String.string) + : parse_nonterminal (G := G) str nonterminal + = true + -> parse_of_item G str (NonTerminal nonterminal). +admit. +Defined. + End wf. + End nonterminals. + End parts. + End general. +End sound. + +Import Coq.Strings.String. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Fixpoint list_to_productions {T} (default : T) (ls : list (string * T)) : string -> T + := match ls with + | nil => fun _ => default + | (str, t)::ls' => fun s => if string_dec str s + then t + else list_to_productions default ls' s + end. + +Fixpoint list_to_grammar {T} (default : productions T) (ls : list (string * productions T)) : grammar T + := {| Start_symbol := hd ""%string (map (@fst _ _) ls); + Lookup := list_to_productions default ls; + Valid_nonterminals := map (@fst _ _) ls |}. + +Section interface. + Context {Char} (G : grammar Char). +Definition production_is_reachable (p : production Char) : Prop. +admit. +Defined. +Definition split_list_is_complete `{HSL : StringLike Char} (str : String) (it : item Char) (its : production Char) + (splits : list nat) + : Prop. +exact (forall n, + n <= length str + -> parse_of_item G (take n str) it + -> parse_of_production G (drop n str) its + -> production_is_reachable (it::its) + -> List.In n splits). +Defined. + + Record Splitter := + { + string_type :> StringLike Char; + splits_for : String -> item Char -> production Char -> list nat; + + string_type_properties :> StringLikeProperties Char; + splits_for_complete : forall str it its, + split_list_is_complete str it its (splits_for str it its) + + }. + Global Existing Instance string_type_properties. + + Record Parser (HSL : StringLike Char) := + { + has_parse : @String Char HSL -> bool; + + has_parse_sound : forall str, + has_parse str = true + -> parse_of_item G str (NonTerminal (Start_symbol G)); + + has_parse_complete : forall str (p : parse_of_item G str (NonTerminal (Start_symbol G))), + Forall_parse_of_item + (fun _ nt => List.In nt (Valid_nonterminals G)) + p + -> has_parse str = true + }. +End interface. + +Module Export ParserImplementation. + +Section implementation. + Context {Char} {G : grammar Char}. + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := + { predata := rdp_list_predata (G := G); + split_string_for_production it its str + := splits_for splitter str it its }. + + Program Definition parser : Parser G splitter + := {| has_parse str := parse_nonterminal (G := G) (data := parser_data) str (Start_symbol G); + has_parse_sound str Hparse := parse_nonterminal_sound G _ _ Hparse; + has_parse_complete str p Hp := _ |}. + Next Obligation. +admit. +Defined. +End implementation. + +End ParserImplementation. + +Section implementation. + Context {Char} {ls : list (String.string * productions Char)}. + Local Notation G := (list_to_grammar (nil::nil) ls) (only parsing). + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := parser_data splitter. + + Goal forall str : @String Char splitter, + let G' := + @BooleanRecognizer.parse_nonterminal Char splitter splitter G parser_data str G = true in + G'. + intros str G'. + Timeout 1 assert (pf' : G' -> Prop) by abstract admit. diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index f85a60264..eb37141bc 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -11,7 +11,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), simpl. intros. match goal with - | [ |- appcontext G[@hd] ] => idtac + | [ |- context G[@hd] ] => idtac end. (* This second example comes from CFGV where inspecting subterms of a diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v index 03af16535..71e3a7518 100644 --- a/test-suite/bugs/closed/4375.v +++ b/test-suite/bugs/closed/4375.v @@ -93,14 +93,15 @@ Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} := | A : foo T -> foo T. Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t := - @A@{i} t (cg@{i} t). + @A@{i} t (cg t). Print cg. Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t := - @A@{i} t (@cb@{i} t) + @A@{i} t (cb t) with cb@{i} (t : Type@{i}) : foo@{i} t := - @A@{i} t (@ca@{i} t). + @A@{i} t (ca t). Print ca. -Print cb.
\ No newline at end of file +Print cb. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v new file mode 100644 index 000000000..3189685ec --- /dev/null +++ b/test-suite/bugs/closed/4416.v @@ -0,0 +1,4 @@ +Goal exists x, x. +Unset Solve Unification Constraints. +unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end. +(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v new file mode 100644 index 000000000..ecebaba81 --- /dev/null +++ b/test-suite/bugs/closed/4450.v @@ -0,0 +1,58 @@ +Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop. + +Polymorphic Axiom unit@{u} : Type@{u}. +Polymorphic Axiom tt@{u} : inhabited unit@{u}. + +Polymorphic Hint Resolve tt : the_lemmas. +Set Printing All. +Set Printing Universes. +Goal inhabited unit. +Proof. + eauto with the_lemmas. +Qed. + +Universe u. +Axiom f : Type@{u} -> Prop. +Lemma fapp (X : Type) : f X -> False. +Admitted. +Polymorphic Axiom funi@{i} : f unit@{i}. + +Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False. + eauto using (fapp unit funi). (* The two fapp's have different universes *) +Qed. + +Hint Resolve (fapp unit funi) : mylems. + +Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False. + eauto with mylems. (* Forces the two fapps at the same level *) +Qed. + +Goal (forall U, f U) -> (f unit -> False) -> False /\ False. + eauto. (* Forces the two fapps at the same level *) +Qed. + +Polymorphic Definition MyType@{i} := Type@{i}. +Universes l m n. +Constraint l < m. +Polymorphic Axiom maketype@{i} : MyType@{i}. + +Goal MyType@{l}. +Proof. + Fail solve [ eauto using maketype@{m} ]. + eauto using maketype. + Undo. + eauto using maketype@{n}. +Qed. + +Axiom foo : forall (A : Type), list A. +Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A. + +Universe x y. +Goal list Type@{x}. +Proof. + eauto using (foo Type). (* Refreshes the term *) + Undo. + eauto using foo. Show Universes. + Undo. + eauto using foop. Show Proof. Show Universes. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4464.v b/test-suite/bugs/closed/4464.v new file mode 100644 index 000000000..f8e9405d9 --- /dev/null +++ b/test-suite/bugs/closed/4464.v @@ -0,0 +1,4 @@ +Goal True -> True. +Proof. + intro H'. + let H := H' in destruct H; try destruct H. diff --git a/test-suite/bugs/closed/4471.v b/test-suite/bugs/closed/4471.v new file mode 100644 index 000000000..36efc42d4 --- /dev/null +++ b/test-suite/bugs/closed/4471.v @@ -0,0 +1,6 @@ +Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 : forall (x : A) (x' : B), P (@pair A B x x')), + @eq (P (@pair A B a b)) (p (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))) + (p0 (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))). +Proof. + intros. + Fail generalize dependent (a, b). diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v new file mode 100644 index 000000000..08628377f --- /dev/null +++ b/test-suite/bugs/closed/4527.v @@ -0,0 +1,267 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1199 lines to +430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, +then from 269 lines to 255 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml +4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. + +Import Coq.Init.Notations. + +Global Set Universe Polymorphism. + +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Inductive True : Type := + I : True. +Module Export Datatypes. + +Set Implicit Arguments. +Notation nat := Coq.Init.Datatypes.nat. +Notation S := Coq.Init.Datatypes.S. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. + +Notation "x * y" := (prod x y) : type_scope. + +Open Scope nat_scope. + +End Datatypes. +Module Export Specif. + +Set Implicit Arguments. + +Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P +proj1_sig }. + +Notation sigT := sig (only parsing). + +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + +Notation projT1 := proj1_sig (only parsing). +Notation projT2 := proj2_sig (only parsing). + +End Specif. +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in +Type@{i}. + +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> +Type@{i}) in Type@{i}. + +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope fibration_scope. +Open Scope function_scope. + +Notation pr1 := projT1. +Notation pr2 := projT2. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left +associativity) : function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. + +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : +type_scope. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B}%type_scope f%function_scope {_} _. +Arguments eissect {A B}%type_scope f%function_scope {_} _. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : +function_scope. + +Inductive Unit : Type1 := + tt : Unit. + +Local Open Scope path_scope. + +Section EquivInverse. + + Context {A B : Type} (f : A -> B) {feq : IsEquiv f}. + + Theorem other_adj (b : B) : eissect f (f^-1 b) = ap f^-1 (eisretr f b). +admit. +Defined. + + Global Instance isequiv_inverse : IsEquiv f^-1 | 10000 + := BuildIsEquiv B A f^-1 f (eissect f) (eisretr f) other_adj. +End EquivInverse. + +Section Adjointify. + + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). +admit. +Defined. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. + +End Adjointify. + + Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. + + Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + + Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : +Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). +Export Os. + +Existing Class In. + + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + +Arguments inO_equiv_inO {O} T {U} {_} f {_}. +Global Existing Instance O_inO. + +Section ORecursion. + Context {O : ReflectiveSubuniverse}. + + Definition O_indpaths {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o to O P == h o to O P) + : g == h + := (fst (snd (extendable_to_O O 2) g h) p).1. + + Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) + : O_indpaths g h p (to O P x) = p x + := (fst (snd (extendable_to_O O 2) g h) p).2 x. + +End ORecursion. + +Section Reflective_Subuniverse. + Universes Ou Oa. + Context (O : ReflectiveSubuniverse@{Ou Oa}). + + Definition inO_isequiv_to_O (T:Type) + : IsEquiv (to O T) -> In O T + := fun _ => inO_equiv_inO (O T) (to O T)^-1. + + Definition inO_to_O_retract (T:Type) (mu : O T -> T) + : Sect (to O T) mu -> In O T. + Proof. + unfold Sect; intros H. + apply inO_isequiv_to_O. + apply isequiv_adjointify with (g:=mu). + - + refine (O_indpaths (to O T o mu) idmap _). + intros x; exact (ap (to O T) (H x)). + - + exact H. + Defined. + + Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : +S) : In@{Ou Oa i} O (x=y). + Proof. + simple refine (inO_to_O_retract@{i} _ _ _); intro u. + - + assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). + { + refine (O_indpaths _ _ _); simpl. + intro v; exact v. +} + exact (p u). + - + hnf. + rewrite O_indpaths_beta; reflexivity. + Qed. + Check inO_paths@{Type}. diff --git a/test-suite/bugs/closed/4529.v b/test-suite/bugs/closed/4529.v new file mode 100644 index 000000000..8b3c24fec --- /dev/null +++ b/test-suite/bugs/closed/4529.v @@ -0,0 +1,45 @@ +(* File reduced by coq-bug-finder from original input, then from 1334 lines to 1518 lines, then from 849 lines to 59 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 22 2016 18:20:47 with OCaml 4.02.3 + coqtop version r-schnelltop:/home/r/src/coq/coq,(HEAD detached at V8.5) (5e23fb90b39dfa014ae5c4fb46eb713cca09dbff) *) +Require Coq.Setoids.Setoid. +Import Coq.Setoids.Setoid. + +Class Equiv A := equiv: relation A. +Infix "≡" := equiv (at level 70, no associativity). +Notation "(≡)" := equiv (only parsing). + +(* If I remove this line, everything compiles. *) +Set Primitive Projections. + +Class Dist A := dist : nat -> relation A. +Notation "x ={ n }= y" := (dist n x y) + (at level 70, n at next level, format "x ={ n }= y"). + +Record CofeMixin A `{Equiv A, Dist A} := { + mixin_equiv_dist x y : x ≡ y <-> forall n, x ={n}= y; + mixin_dist_equivalence n : Equivalence (dist n); +}. + +Structure cofeT := CofeT { + cofe_car :> Type; + cofe_equiv : Equiv cofe_car; + cofe_dist : Dist cofe_car; + cofe_mixin : CofeMixin cofe_car +}. +Existing Instances cofe_equiv cofe_dist. +Arguments cofe_car : simpl never. + +Section cofe_mixin. + Context {A : cofeT}. + Implicit Types x y : A. + Lemma equiv_dist x y : x ≡ y <-> forall n, x ={n}= y. +Admitted. +End cofe_mixin. + Context {A : cofeT}. + Global Instance cofe_equivalence : Equivalence ((≡) : relation A). + Proof. + split. + * + intros x. +apply equiv_dist. + diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 048f31ce3..da140c931 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -652,7 +652,7 @@ Defined. Definition ReflectiveSubuniverse := Modality. - Definition O_reflector := O_reflector. + Definition O_reflector@{u a i} := O_reflector@{u a i}. Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), Type2le@{i a} -> Type2le@{i a} @@ -660,7 +660,7 @@ Defined. Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), In@{u a i} O (O_reflector@{u a i} O T) := O_inO@{u a i}. - Definition to := to. + Definition to@{u a i} := to@{u a i}. Definition inO_equiv_inO@{u a i j k} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), diff --git a/test-suite/bugs/closed/4622.v b/test-suite/bugs/closed/4622.v new file mode 100644 index 000000000..ffa478cb8 --- /dev/null +++ b/test-suite/bugs/closed/4622.v @@ -0,0 +1,24 @@ +Set Primitive Projections. + +Record foo : Type := bar { x : unit }. + +Goal forall t u, bar t = bar u -> t = u. +Proof. + intros. + injection H. + trivial. +Qed. +(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *) + +(** Dependent pattern-matching is ok on this one as it has eta *) +Definition baz (x : foo) := + match x as x' return x' = x' with + | bar u => eq_refl + end. + +Inductive foo' : Type := bar' {x' : unit; y: foo'}. +(** Dependent pattern-matching is not ok on this one *) +Fail Definition baz' (x : foo') := + match x as x' return x' = x' with + | bar' u y => eq_refl + end. diff --git a/test-suite/bugs/closed/4653.v b/test-suite/bugs/closed/4653.v new file mode 100644 index 000000000..4514342c5 --- /dev/null +++ b/test-suite/bugs/closed/4653.v @@ -0,0 +1,3 @@ +Definition T := Type. +Module Type S. Parameter foo : let A := T in True. End S. +Module M <: S. Lemma foo (A := T) : True. Proof I. End M. diff --git a/test-suite/bugs/closed/4661.v b/test-suite/bugs/closed/4661.v new file mode 100644 index 000000000..03d2350a6 --- /dev/null +++ b/test-suite/bugs/closed/4661.v @@ -0,0 +1,10 @@ +Module Type Test. + Parameter t : Type. +End Test. + +Module Type Func (T:Test). + Parameter x : Type. +End Func. + +Module Shortest_path (T : Test). +Print Func. diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v new file mode 100644 index 000000000..1ae508185 --- /dev/null +++ b/test-suite/bugs/closed/4673.v @@ -0,0 +1,57 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3 + coqtop version 8.5 (February 2016) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Lists.List. +Import Coq.Lists.List. +Import Coq.Classes.Morphisms. + +Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs)) + ls + : P ls + := match ls with + | nil => N + | x::xs => C x xs + end. + +Global Instance list_caset_Proper' {A P} + : Proper (eq + ==> pointwise_relation _ (pointwise_relation _ eq) + ==> eq + ==> eq) + (@list_caset A (fun _ => P)). +admit. +Defined. + +Global Instance list_caset_Proper'' {A P} + : (Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> forall_relation (fun _ => eq)) + (list_caset A (fun _ => P))). +Admitted. + +Goal forall (Char : Type) (P : forall _ : list bool, Prop) (l : list bool) (l0 : forall _ : forall _ : Char, bool, list bool) + + (T : Type) (T0 : forall _ : T, Type) (t : T), + + let predata := t in + + forall (splitdata : T0 predata) (l5 : forall _ : T0 t, list nat) (T1 : Type) (b : forall (_ : T1) (_ : Char), bool) + + (T2 : Type) (a11 : T2) (xs : list T2) (T3 : Type) (i0 : T3) (P0 : Set) (b1 : forall (_ : nat) (_ : P0), bool) + + (l2 : forall (_ : forall _ : T1, list bool) (_ : forall _ : P0, list bool) (_ : T2), list bool) + + (l1 : forall (_ : forall _ : forall _ : Char, bool, list bool) (_ : forall _ : P0, list bool) (_ : T3), list bool) + + (_ : forall NT : forall _ : P0, list bool, @eq (list bool) (l1 l0 NT i0) (l2 (fun f : T1 => l0 (b f)) NT a11)), + + P + (@list_caset T2 (fun _ : list T2 => list bool) l + (fun (_ : T2) (_ : list T2) => l1 l0 (fun a9 : P0 => @map nat bool (fun x0 : nat => b1 x0 a9) (l5 splitdata)) i0 +) xs). + intros. + subst predata; + let H := match goal with H : forall _, _ = _ |- _ => H end in + setoid_rewrite H || fail 0 "too early". + Undo. + setoid_rewrite H. diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v new file mode 100644 index 000000000..c94fa31a9 --- /dev/null +++ b/test-suite/bugs/closed/4679.v @@ -0,0 +1,18 @@ +Require Import Coq.Setoids.Setoid. +Goal forall (T : nat -> Set -> Set) (U : Set) + (H : forall n : nat, T n (match n with + | 0 => fun x => x + | S _ => fun x => x + end (nat = nat)) = U), + T 0 (nat = nat) = U. +Proof. + intros. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + rewrite H || fail 0 "too early". + Undo. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + setoid_rewrite (H 0) || fail 0 "too early". + Undo. + setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *) + reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v new file mode 100644 index 000000000..9c0bed42c --- /dev/null +++ b/test-suite/bugs/closed/4684.v @@ -0,0 +1,32 @@ +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. + +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v new file mode 100644 index 000000000..888481210 --- /dev/null +++ b/test-suite/bugs/closed/4723.v @@ -0,0 +1,28 @@ + +Require Coq.Program.Tactics. + +Record Matrix (m n : nat). + +Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q): + Matrix (m*p) (n*q). Admitted. + +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Ltac Obligation Tactic := admit. +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Axiom cheat : forall {A}, A. +Obligation Tactic := apply cheat. + +Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. +admit. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v new file mode 100644 index 000000000..fd5e0fb60 --- /dev/null +++ b/test-suite/bugs/closed/4725.v @@ -0,0 +1,38 @@ +Require Import EquivDec Equivalence List Program. +Require Import Relation_Definitions. +Import ListNotations. +Generalizable All Variables. + +Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V +:= + match l with + | nil => nil + | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl) + end. + +Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (xs : list V) (x : V) : + length (removeV x xs) < length (x :: xs). + Proof. Admitted. + +(* Function version *) +Set Printing Universes. + +Require Import Recdef. + +Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (l : list V) { measure length l} := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) + end. +Proof. intros. apply remove_le. Qed. + +(* Program version *) + +Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V) + { measure (@length V l) lt } := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _ + end. diff --git a/test-suite/bugs/closed/4726.v b/test-suite/bugs/closed/4726.v new file mode 100644 index 000000000..0037b6fde --- /dev/null +++ b/test-suite/bugs/closed/4726.v @@ -0,0 +1,19 @@ +Set Universe Polymorphism. + +Definition le@{i j} : Type@{j} := + (fun A : Type@{j} => A) + (unit : Type@{i}). +Definition eq@{i j} : Type@{j} := let x := le@{i j} in le@{j i}. + +Record Inj@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{j} := + { inj : A }. + +Monomorphic Universe u1. +Let ty1 : Type@{u1} := Set. +Check Inj@{Set u1}. +(* Would fail with univ inconsistency if the universe was minimized *) + +Record Inj'@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{j} := + { inj' : A; foo : Type@{j} := eq@{i j} }. +Fail Check Inj'@{Set u1}. (* Do not drop constraint i = j *) +Check Inj'@{Set Set}. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v new file mode 100644 index 000000000..a6ebda61c --- /dev/null +++ b/test-suite/bugs/closed/4733.v @@ -0,0 +1,52 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. + +(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. + +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. +(* Now these all work, but not so in 8.4. If we get the ability to remove notations, this section can also just be removed. *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/closed/4754.v b/test-suite/bugs/closed/4754.v new file mode 100644 index 000000000..5bb3cd1be --- /dev/null +++ b/test-suite/bugs/closed/4754.v @@ -0,0 +1,35 @@ + +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. +Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + setoid_rewrite (FG _ _); [ | reflexivity.. ]. + Undo. + setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v new file mode 100644 index 000000000..7a87b07a8 --- /dev/null +++ b/test-suite/bugs/closed/4762.v @@ -0,0 +1,24 @@ +Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q. + +Lemma foo P Q R : R = myand P Q -> P -> Q -> R. +Proof. intros ->; constructor; auto. Qed. + +Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test1. +Qed. + +Hint Extern 0 => + match goal with + | |- myand _ _ => eapply foo; [reflexivity| |] + end : test2. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test2. (* works *) +Qed. + diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v new file mode 100644 index 000000000..ae8ed0e6e --- /dev/null +++ b/test-suite/bugs/closed/4763.v @@ -0,0 +1,13 @@ +Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. +Coercion is_true : bool >-> Sortclass. +Global Instance: Transitive leb. +Admitted. + +Goal forall x y z, leb x y -> leb y z -> True. + intros ??? H H'. + lazymatch goal with + | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] + => pose proof (transitivity H H' : is_true (R x z)) + end. + exact I. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4764.v b/test-suite/bugs/closed/4764.v new file mode 100644 index 000000000..e545cc1b7 --- /dev/null +++ b/test-suite/bugs/closed/4764.v @@ -0,0 +1,5 @@ +Notation prop_fun x y := (fun (x : Prop) => y). +Definition foo := fun (p : Prop) => p. +Definition bar := fun (_ : Prop) => O. +Print foo. +Print bar. diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v new file mode 100644 index 000000000..d87906f31 --- /dev/null +++ b/test-suite/bugs/closed/4769.v @@ -0,0 +1,94 @@ + +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) +(* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3 + coqtop version trunk (June 2016) *) + +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Reserved Notation "x * y" (at level 40, left associativity). +Delimit Scope type_scope with type. +Open Scope type_scope. +Global Set Universe Polymorphism. +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Set Implicit Arguments. +Global Set Nonrecursive Elimination Schemes. +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Notation "x * y" := (prod x y) : type_scope. +Axiom admit : forall {T}, T. +Delimit Scope function_scope with function. +Notation compose := (fun g f x => g (f x)). +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope. +Record PreCategory := + Build_PreCategory { + object :> Type; + morphism : object -> object -> Type; + identity : forall x, morphism x x }. +Bind Scope category_scope with PreCategory. +Record Functor (C D : PreCategory) := { object_of :> C -> D }. +Bind Scope functor_scope with Functor. +Class Isomorphic {C : PreCategory} (s d : C) := {}. +Definition oppositeC (C : PreCategory) : PreCategory + := @Build_PreCategory C (fun s d => morphism C d s) admit. +Notation "C ^op" := (oppositeC C) (at level 3, format "C '^op'") : category_scope. +Definition oppositeF C D (F : Functor C D) : Functor C^op D^op + := Build_Functor (C^op) (D^op) (object_of F). +Definition set_cat : PreCategory := @Build_PreCategory Type (fun x y => x -> y) admit. +Definition prodC (C D : PreCategory) : PreCategory + := @Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + admit. +Infix "*" := prodC : category_scope. +Section composition. + Variables B C D E : PreCategory. + Definition composeF (G : Functor D E) (F : Functor C D) : Functor C E := Build_Functor C E (fun c => G (F c)). +End composition. +Infix "o" := composeF : functor_scope. +Definition fstF {C D} : Functor (C * D) C := admit. +Definition sndF {C D} : Functor (C * D) D := admit. +Definition prodF C D D' (F : Functor C D) (F' : Functor C D') : Functor C (D * D') := admit. +Local Infix "*" := prodF : functor_scope. +Definition pairF C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D') + := (F o fstF) * (F' o sndF). +Section hom_functor. + Variable C : PreCategory. + Local Notation obj_of c'c := + ((morphism + C + (fst (c'c : object (C^op * C))) + (snd (c'c : object (C^op * C))))). + Definition hom_functor : Functor (C^op * C) set_cat + := Build_Functor (C^op * C) set_cat (fun c'c => obj_of c'c). +End hom_functor. +Definition identityF C : Functor C C := admit. +Definition functor_category (C D : PreCategory) : PreCategory + := @Build_PreCategory (Functor C D) admit admit. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Definition NaturalIsomorphism (C D : PreCategory) F G := @Isomorphic (C -> D) F G. + +Section Adjunction. + Variables C D : PreCategory. + Variable F : Functor C D. + Variable G : Functor D C. + + Record AdjunctionHom := + { + mate_of : @NaturalIsomorphism + (prodC (oppositeC C) D) + (@set_cat) + (@composeF + (prodC (oppositeC C) D) + (prodC (oppositeC D) D) + (@set_cat) (@hom_functor D) + (@pairF (oppositeC C) + (oppositeC D) D D + (@oppositeF C D F) (identityF D))) + (@composeF + (prodC (oppositeC C) D) + (prodC (oppositeC C) C) + (@set_cat) (@hom_functor C) + (@pairF (oppositeC C) + (oppositeC C) D C + (identityF (oppositeC C)) G)) + }. +End Adjunction.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4780.v b/test-suite/bugs/closed/4780.v new file mode 100644 index 000000000..4cec43184 --- /dev/null +++ b/test-suite/bugs/closed/4780.v @@ -0,0 +1,106 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1889 lines to 144 lines, then from 158 lines to 144 lines *) +(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 + coqtop version 8.5pl1 (April 2016) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Global Set Universe Polymorphism. +Global Set Asymmetric Patterns. +Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..)) + (at level 200, x binder, right associativity, + format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") + : type_scope. +Definition relation (A : Type) := A -> A -> Type. +Class Transitive {A} (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z. +Tactic Notation "etransitivity" open_constr(y) := + let R := match goal with |- ?R ?x ?z => constr:(R) end in + let x := match goal with |- ?R ?x ?z => constr:(x) end in + let z := match goal with |- ?R ?x ?z => constr:(z) end in + refine (@transitivity _ R _ x y z _ _). +Tactic Notation "etransitivity" := etransitivity _. +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation pr1 := projT1. +Notation pr2 := projT2. +Notation "x .1" := (projT1 x) (at level 3) : fibration_scope. +Notation "x .2" := (projT2 x) (at level 3) : fibration_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. +Arguments paths_rect [A] a P f y p. +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. +Delimit Scope path_scope with path. +Local Open Scope path_scope. +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. +Instance transitive_paths {A} : Transitive (@paths A) | 0 := @concat A. +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. +Notation "1" := idpath : path_scope. +Notation "p @ q" := (concat p q) (at level 20) : path_scope. +Notation "p ^" := (inverse p) (at level 3) : path_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): + p # (f x) = f y + := match p with idpath => idpath end. +Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B) + (p : x = y) (z : P (f x)) + : transport (fun x => P (f x)) p z = transport P (ap f p) z. +admit. +Defined. +Local Open Scope path_scope. +Generalizable Variables X A B C f g n. +Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (pq : {p : u.1 = v.1 & p # u.2 = v.2}) + : u = v + := match pq with + | existT p q => + match u, v return (forall p0 : (u.1 = v.1), (p0 # u.2 = v.2) -> (u=v)) with + | (x;y), (x';y') => fun p1 q1 => + match p1 in (_ = x'') return (forall y'', (p1 # y = y'') -> (x;y)=(x'';y'')) with + | idpath => fun y' q2 => + match q2 in (_ = y'') return (x;y) = (x;y'') with + | idpath => 1 + end + end y' q1 + end p q + end. +Definition path_sigma {A : Type} (P : A -> Type) (u v : sigT P) + (p : u.1 = v.1) (q : p # u.2 = v.2) + : u = v + := path_sigma_uncurried P u v (p;q). +Definition projT1_path `{P : A -> Type} {u v : sigT P} (p : u = v) + : u.1 = v.1 + := + ap (@projT1 _ _) p. +Notation "p ..1" := (projT1_path p) (at level 3) : fibration_scope. +Definition projT2_path `{P : A -> Type} {u v : sigT P} (p : u = v) + : p..1 # u.2 = v.2 + := (transport_compose P (@projT1 _ _) p u.2)^ + @ (@apD {x:A & P x} _ (@projT2 _ _) _ _ p). +Notation "p ..2" := (projT2_path p) (at level 3) : fibration_scope. +Definition eta_path_sigma_uncurried `{P : A -> Type} {u v : sigT P} + (p : u = v) + : path_sigma_uncurried _ _ _ (p..1; p..2) = p. +admit. +Defined. +Definition eta_path_sigma `{P : A -> Type} {u v : sigT P} (p : u = v) + : path_sigma _ _ _ (p..1) (p..2) = p + := eta_path_sigma_uncurried p. + +Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (p q : u = v) + (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2}) + : p = q. +Proof. + destruct rs, p, u. + etransitivity; [ | apply eta_path_sigma ]. + simpl in *. + induction p0. + admit. +Defined. + diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v index ed4443786..dbd71035d 100644 --- a/test-suite/bugs/closed/4782.v +++ b/test-suite/bugs/closed/4782.v @@ -7,3 +7,18 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. Goal p. Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. +(* A simplification of an example from coquelicot, which was failing + at some time after a fix #4782 was committed. *) + +Record T := { dom : Type }. +Definition pairT A B := {| dom := (dom A * dom B)%type |}. +Class C (A:Type). +Parameter B:T. +Instance c (A:T) : C (dom A). +Instance cn : C (dom B). +Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A. +Set Typeclasses Debug. +Goal forall (A:T) (x:dom A), pairT A A = pairT A A. +intros. +apply (F _ _) with (x,x). + diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v new file mode 100644 index 000000000..c3c97d3f5 --- /dev/null +++ b/test-suite/bugs/closed/4785.v @@ -0,0 +1,45 @@ +Require Coq.Lists.List Coq.Vectors.Vector. +Require Coq.Compat.Coq85. + +Module A. +Import Coq.Lists.List Coq.Vectors.Vector. +Import ListNotations. +Check [ ]%list : list _. +Import VectorNotations ListNotations. +Delimit Scope vector_scope with vector. +Check [ ]%vector : Vector.t _ _. +Check []%vector : Vector.t _ _. +Check [ ]%list : list _. +Check []%list : list _. + +Goal True. + idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *) +Abort. + +Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Arguments mynil {_}, _. +Arguments mycons {_} _ _. +Notation " [] " := mynil (compat "8.5") : mylist_scope. +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x nil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. + +Import Coq.Compat.Coq85. +Locate Module VectorNotations. +Import VectorDef.VectorNotations. + +Check []%vector : Vector.t _ _. +Check []%mylist : mylist _. +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +End A. + +Module B. +Import Coq.Compat.Coq85. + +Goal True. + idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) +Abort. +End B. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v new file mode 100644 index 000000000..9d65840ac --- /dev/null +++ b/test-suite/bugs/closed/4785_compat_85.v @@ -0,0 +1,46 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *) +Require Coq.Lists.List Coq.Vectors.Vector. +Require Coq.Compat.Coq85. + +Module A. +Import Coq.Lists.List Coq.Vectors.Vector. +Import ListNotations. +Check [ ]%list : list _. +Import VectorNotations ListNotations. +Delimit Scope vector_scope with vector. +Check [ ]%vector : Vector.t _ _. +Check []%vector : Vector.t _ _. +Check [ ]%list : list _. +Fail Check []%list : list _. + +Goal True. + idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) +Abort. + +Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Arguments mynil {_}, _. +Arguments mycons {_} _ _. +Notation " [] " := mynil (compat "8.5") : mylist_scope. +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x nil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. + +Import Coq.Compat.Coq85. +Locate Module VectorNotations. +Import VectorDef.VectorNotations. + +Check []%vector : Vector.t _ _. +Check []%mylist : mylist _. +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +End A. + +Module B. +Import Coq.Compat.Coq85. + +Goal True. + idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) +Abort. +End B. diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v new file mode 100644 index 000000000..dbc3d46fc --- /dev/null +++ b/test-suite/bugs/closed/4798.v @@ -0,0 +1,3 @@ +Check match 2 with 0 => 0 | S n => n end. +Notation "|" := 1 (compat "8.4"). +Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v new file mode 100644 index 000000000..a91496262 --- /dev/null +++ b/test-suite/bugs/closed/4811.v @@ -0,0 +1,1685 @@ +(* Test about a slowness of f_equal in 8.5pl1 *) + +(* Submitted by Jason Gross *) + +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) +(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) +(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 + coqtop version 8.5pl1 (April 2016) *) +Require Coq.ZArith.ZArith. + +Import Coq.ZArith.ZArith. + +Axiom F : Z -> Set. +Definition Let_In {A P} (x : A) (f : forall y : A, P y) + := let y := x in f y. +Local Open Scope Z_scope. +Definition modulus : Z := 2^255 - 19. +Axiom decode : list Z -> F modulus. +Goal forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z, + let Zmul := Z.mul in + let Zadd := Z.add in + let Zsub := Z.sub in + let Zpow_pos := Z.pow_pos in + @eq (F (Zsub (Zpow_pos (Zpos (xO xH)) (xI (xI (xI (xI (xI (xI (xI xH)))))))) (Zpos (xI (xI (xO (xO xH))))))) + (@decode + (@Let_In Z (fun _ : Z => list Z) + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) (Zmul (Zmul x7 y3) (Zpos (xO xH)))) + (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) + (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (fun z : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) + (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) + (fun z0 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z0 (Zpos (xI (xO (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (fun z1 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z1 (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) + (Zmul x4 y9))))) + (fun z2 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z2 (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) + (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) + (fun z3 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z3 (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) + (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) + (fun z4 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z4 (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) + (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) + (Zmul x0 y6)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) + (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) + (fun z5 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z5 (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) + (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) + (fun z6 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z6 (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) + (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) + (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) + (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) + (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) + (fun z7 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Z.shiftr z7 (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) + (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) + (Zmul x1 y8)) (Zmul x0 y9))) + (fun z8 : Z => + @Let_In Z (fun _ : Z => list Z) + (Zadd (Zmul (Zpos (xI (xI (xO (xO xH))))) (Z.shiftr z8 (Zpos (xI (xO (xO (xI xH))))))) + (Z.land z + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) + (fun z9 : Z => + @cons Z + (Z.land z9 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Zadd (Z.shiftr z9 (Zpos (xO (xI (xO (xI xH)))))) + (Z.land z0 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land z1 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land z2 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@cons Z + (Z.land z3 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land z4 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@cons Z + (Z.land z5 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land z6 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@cons Z + (Z.land z7 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land z8 + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@nil Z))))))))))))))))))))))) + (@decode + (@cons Z + (Z.land + (Zadd + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul + (Zmul x9 y1) + (Zpos (xO xH))) + (Zmul x8 y2)) + (Zmul + (Zmul x7 y3) + (Zpos (xO xH)))) + (Zmul x6 y4)) + (Zmul (Zmul x5 y5) (Zpos (xO xH)))) + (Zmul x4 y6)) + (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) + (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul x9 y2) (Zmul x8 y3)) + (Zmul x7 y4)) + (Zmul x6 y5)) + (Zmul x5 y6)) + (Zmul x4 y7)) (Zmul x3 y8)) + (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) + (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) + (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) + (Zmul x6 y6)) + (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) + (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) + (Zmul x6 y7)) (Zmul x5 y8)) + (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) + (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) + (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) + (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) + (Zmul x1 y4)) (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) + (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) + (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) + (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) + (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) + (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) + (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) + (Zmul x0 y8)) (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) (Zmul x5 y4)) + (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) + (Zpos (xI (xO (xO (xI xH))))))) + (Z.land + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) + (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) + (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Zadd + (Z.shiftr + (Zadd + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul + (Zmul x9 y1) + (Zpos (xO xH))) + (Zmul x8 y2)) + (Zmul + (Zmul x7 y3) + (Zpos (xO xH)))) + (Zmul x6 y4)) + (Zmul + (Zmul x5 y5) + (Zpos (xO xH)))) + (Zmul x4 y6)) + (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) + (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul x9 y2) + (Zmul x8 y3)) + (Zmul x7 y4)) + (Zmul x6 y5)) + (Zmul x5 y6)) + (Zmul x4 y7)) + (Zmul x3 y8)) + (Zmul x2 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zmul x2 y0) + (Zmul (Zmul x1 y1) (Zpos (xO xH)))) + (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul (Zmul x9 y3) (Zpos (xO xH))) + (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) + (Zmul x6 y6)) + (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) + (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) + (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) + (Zmul x7 y6)) (Zmul x6 y7)) + (Zmul x5 y8)) (Zmul x4 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) + (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) + (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) + (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) + (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) + (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) + (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) + (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) + (Zmul x0 y6)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) + (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) + (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) + (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) + (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) + (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) + (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) + (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) + (Zmul x1 y8)) (Zmul x0 y9))) (Zpos (xI (xO (xO (xI xH))))))) + (Z.land + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) + (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Z.land + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) + (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) + (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) + (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) + (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) + (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) + (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) + (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) + (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) + (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) + (Zmul x4 y9))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) + (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) + (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) + (Zmul x6 y5)) (Zmul x5 y6)) (Zmul x4 y7)) + (Zmul x3 y8)) (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) + (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) + (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) + (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) + (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) + (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) + (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) + (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) + (Zmul x6 y5)) (Zmul x5 y6)) + (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) + (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) + (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) + (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) + (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) + (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul (Zmul x9 y1) (Zpos (xO xH))) + (Zmul x8 y2)) + (Zmul (Zmul x7 y3) (Zpos (xO xH)))) + (Zmul x6 y4)) + (Zmul (Zmul x5 y5) (Zpos (xO xH)))) + (Zmul x4 y6)) + (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) + (Zmul x7 y4)) (Zmul x6 y5)) + (Zmul x5 y6)) (Zmul x4 y7)) + (Zmul x3 y8)) (Zmul x2 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) + (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) + (Zmul x8 y4)) (Zmul (Zmul x7 y5) (Zpos (xO xH)))) + (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) + (Zmul x6 y7)) (Zmul x5 y8)) (Zmul x4 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) + (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) + (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) + (Zmul x1 y4)) (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) + (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) + (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) + (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul + (Zmul x9 y1) + (Zpos (xO xH))) + (Zmul x8 y2)) + (Zmul + (Zmul x7 y3) + (Zpos (xO xH)))) + (Zmul x6 y4)) + (Zmul (Zmul x5 y5) (Zpos (xO xH)))) + (Zmul x4 y6)) + (Zmul (Zmul x3 y7) (Zpos (xO xH)))) + (Zmul x2 y8)) + (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul x9 y2) (Zmul x8 y3)) + (Zmul x7 y4)) + (Zmul x6 y5)) + (Zmul x5 y6)) + (Zmul x4 y7)) (Zmul x3 y8)) + (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) + (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) + (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) + (Zmul x6 y6)) + (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) + (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) + (Zmul x6 y7)) (Zmul x5 y8)) + (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) + (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) + (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) + (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) + (Zmul x1 y4)) (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) + (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) + (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) + (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) + (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul + (Zmul x9 y1) + (Zpos (xO xH))) + (Zmul x8 y2)) + (Zmul + (Zmul x7 y3) + (Zpos (xO xH)))) + (Zmul x6 y4)) + (Zmul + (Zmul x5 y5) + (Zpos (xO xH)))) + (Zmul x4 y6)) + (Zmul + (Zmul x3 y7) + (Zpos (xO xH)))) + (Zmul x2 y8)) + (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul x9 y2) + (Zmul x8 y3)) + (Zmul x7 y4)) + (Zmul x6 y5)) + (Zmul x5 y6)) + (Zmul x4 y7)) + (Zmul x3 y8)) + (Zmul x2 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zmul x2 y0) + (Zmul (Zmul x1 y1) (Zpos (xO xH)))) + (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul + (Zmul x9 y3) + (Zpos (xO xH))) + (Zmul x8 y4)) + (Zmul (Zmul x7 y5) (Zpos (xO xH)))) + (Zmul x6 y6)) + (Zmul (Zmul x5 y7) (Zpos (xO xH)))) + (Zmul x4 y8)) + (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) + (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) + (Zmul x7 y6)) (Zmul x6 y7)) + (Zmul x5 y8)) (Zmul x4 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) + (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) + (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) + (Zmul x8 y6)) (Zmul (Zmul x7 y7) (Zpos (xO xH)))) + (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) + (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) + (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) + (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) + (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) + (Zmul x0 y6)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) + (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) + (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) + (Zmul x1 y6)) (Zmul x0 y7)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) + (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) + (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) + (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) + (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) + (@cons Z + (Z.land + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd + (Z.shiftr + (Zadd (Zmul x0 y0) + (Zmul + (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul + (Zmul x9 y1) + (Zpos (xO xH))) + (Zmul x8 y2)) + (Zmul + (Zmul x7 y3) + (Zpos (xO xH)))) + (Zmul x6 y4)) + (Zmul + (Zmul x5 y5) + (Zpos (xO xH)))) + (Zmul x4 y6)) + (Zmul + (Zmul x3 y7) + (Zpos (xO xH)))) + (Zmul x2 y8)) + (Zmul + (Zmul x1 y9) + (Zpos (xO xH)))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul x9 y2) + (Zmul x8 y3)) + (Zmul x7 y4)) + (Zmul x6 y5)) + (Zmul x5 y6)) + (Zmul x4 y7)) + (Zmul x3 y8)) + (Zmul x2 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zmul x2 y0) + (Zmul (Zmul x1 y1) (Zpos (xO xH)))) + (Zmul x0 y2)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zmul + (Zmul x9 y3) + (Zpos (xO xH))) + (Zmul x8 y4)) + (Zmul + (Zmul x7 y5) + (Zpos (xO xH)))) + (Zmul x6 y6)) + (Zmul + (Zmul x5 y7) + (Zpos (xO xH)))) + (Zmul x4 y8)) + (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) + (Zmul x1 y2)) (Zmul x0 y3)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul x9 y4) (Zmul x8 y5)) + (Zmul x7 y6)) + (Zmul x6 y7)) + (Zmul x5 y8)) + (Zmul x4 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul x4 y0) + (Zmul (Zmul x3 y1) (Zpos (xO xH)))) + (Zmul x2 y2)) + (Zmul (Zmul x1 y3) (Zpos (xO xH)))) + (Zmul x0 y4)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd + (Zadd + (Zadd + (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) + (Zmul x8 y6)) + (Zmul (Zmul x7 y7) (Zpos (xO xH)))) + (Zmul x6 y8)) + (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) + (Zmul x2 y3)) (Zmul x1 y4)) + (Zmul x0 y5)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) + (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zmul x6 y0) + (Zmul (Zmul x5 y1) (Zpos (xO xH)))) + (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) + (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) + (Zmul x0 y6)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) + (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) + (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) + (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) + (Zmul x1 y6)) (Zmul x0 y7)) + (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) + (Zpos (xI (xO (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) + (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) + (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) + (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) + (Zmul x0 y8)) + (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) + (Zpos (xO (xI (xO (xI xH)))))) + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd + (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) + (Zmul x6 y3)) (Zmul x5 y4)) (Zmul x4 y5)) + (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) + (Zpos + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI + (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) + (@nil Z)))))))))))). + cbv beta zeta. + intros. + (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early". + Undo. + Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *) diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v index 86597c88f..00a523842 100644 --- a/test-suite/bugs/closed/4816.v +++ b/test-suite/bugs/closed/4816.v @@ -15,3 +15,15 @@ Section Foo. Fail Constraint X <= Z. End Bar. End Foo. + +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +Section qux. + Polymorphic Universes A. + Section bar. + Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + End bar. +End qux. diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v new file mode 100644 index 000000000..904abb228 --- /dev/null +++ b/test-suite/bugs/closed/4818.v @@ -0,0 +1,24 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *) +(* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *) +(* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3 + coqtop version 8.5pl1 (June 2016) *) +Set Universe Polymorphism. + +Inductive GCov (I : Type) : Type := | Foo : I -> GCov I. + +Section Product. + +Variables S IS : Type. +Variable locS : IS -> True. + +Goal GCov (IS * S) -> GCov IS. +intros X0. induction X0; intros. +destruct i. +specialize (locS i). +clear -locS. +destruct locS. Show Universes. +Admitted. + +(* +Anomaly: Universe Product.5189 undefined. Please report. +*) diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v new file mode 100644 index 000000000..a2fa93832 --- /dev/null +++ b/test-suite/bugs/closed/4858.v @@ -0,0 +1,7 @@ +Require Import Nsatz. +Goal True. +try nsatz_compute + (PEc 0%Z :: PEc (-1)%Z + :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1 + :: PEsub (PEX Z 1) (PEX Z 1) :: nil). +Abort. diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v new file mode 100644 index 000000000..1e47f2957 --- /dev/null +++ b/test-suite/bugs/closed/4863.v @@ -0,0 +1,33 @@ +Require Import Classes.DecidableClass. + +Inductive Foo : Set := +| foo1 | foo2. + +Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. +Proof. + intros P H. + refine (Build_Decidable _ (if H then true else false) _). + intuition congruence. +Qed. + +Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances. + +Goal forall (a b : Foo), {a=b}+{a<>b}. +intros. +abstract (abstract (decide equality)). (*abstract works here*) +Qed. + +Check ltac:(abstract (exact I)) : True. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. typeclasses eauto. +typeclasses eauto. Qed. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. +refine _. +refine _. +Defined. +(*fails*) diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v new file mode 100644 index 000000000..c5bf3289b --- /dev/null +++ b/test-suite/bugs/closed/4865.v @@ -0,0 +1,52 @@ +(* Check discharge of arguments scopes + other checks *) + +(* This is bug #4865 *) + +Notation "<T>" := true : bool_scope. +Section A. + Check negb <T>. + Global Arguments negb : clear scopes. + Fail Check negb <T>. +End A. + +(* Check that no scope is re-computed *) +Fail Check negb <T>. + +(* Another test about arguments scopes in sections *) + +Notation "0" := true. +Section B. + Variable x : nat. + Let T := nat -> nat. + Definition f y : T := fun z => x + y + z. + Fail Check f 1 0. (* 0 in nat, 0 in bool *) + Fail Check f 0 0. (* 0 in nat, 0 in bool *) + Check f 0 1. (* 0 and 1 in nat *) + Global Arguments f _%nat_scope _%nat_scope. + Check f 0 0. (* both 0 in nat *) +End B. + +(* Check that only the scope for the extra product on x is re-computed *) +Check f 0 0 0. (* All 0 in nat *) + +Section C. + Variable x : nat. + Let T := nat -> nat. + Definition g y : T := fun z => x + y + z. + Global Arguments g : clear scopes. + Check g 1. (* 1 in nat *) +End C. + +(* Check that only the scope for the extra product on x is re-computed *) +Check g 0. (* 0 in nat *) +Fail Check g 0 1 0. (* 2nd 0 in bool *) +Fail Check g 0 0 1. (* 2nd 0 in bool *) + +(* Another test on arguments scopes: checking scope for expanding arities *) +(* Not sure this is very useful, but why not *) + +Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end. +Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end. +Notation "0" := true. +Arguments Scope lam [nat_scope nat_scope]. +Check (lam 1 0). diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v new file mode 100644 index 000000000..6d21b66fe --- /dev/null +++ b/test-suite/bugs/closed/4869.v @@ -0,0 +1,18 @@ +Universes i. + +Fail Constraint i < Set. +Fail Constraint i <= Set. +Fail Constraint i = Set. +Constraint Set <= i. +Constraint Set < i. +Fail Constraint i < j. (* undeclared j *) +Fail Constraint i < Type. (* anonymous *) + +Set Universe Polymorphism. + +Section Foo. + Universe j. + Constraint Set < j. + + Definition foo := Type@{j}. +End Foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v new file mode 100644 index 000000000..f2f917b4e --- /dev/null +++ b/test-suite/bugs/closed/4873.v @@ -0,0 +1,72 @@ +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. +Require Import Coq.Compat.Coq85. + +Fixpoint tuple' T n : Type := + match n with + | O => T + | S n' => (tuple' T n' * T)%type + end. + +Definition tuple T n : Type := + match n with + | O => unit + | S n' => tuple' T n' + end. + +Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T := + match n with + | 0 => fun x => (x::nil)%list + | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list + end. + +Definition to_list {T} (n:nat) : tuple T n -> list T := + match n with + | 0 => fun _ => nil + | S n' => fun xs : tuple T (S n') => to_list' n' xs + end. + +Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n := + match n return _ with + | 0 => + match xs return (length xs = 0 -> tuple' T 0) with + | nil => fun _ => y + | _ => _ (* impossible *) + end + | S n' => + match xs return (length xs = S n' -> tuple' T (S n')) with + | cons x xs' => fun _ => (from_list' x n' xs' _, y) + | _ => _ (* impossible *) + end + end. +Goal True. + pose from_list'_obligation_3 as e. + repeat (let e' := fresh in + rename e into e'; + (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e); + subst e'). + progress hnf in e. + pose (eq_refl : e = eq_refl). + exact I. +Qed. + +Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n := +match n return _ with +| 0 => + match xs return (length xs = 0 -> tuple T 0) with + | nil => fun _ : 0 = 0 => tt + | _ => _ (* impossible *) + end +| S n' => + match xs return (length xs = S n' -> tuple T (S n')) with + | cons x xs' => fun _ => from_list' x n' xs' _ + | _ => _ (* impossible *) + end +end. + +Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs. +Proof. + destruct xs; simpl; intros; subst; auto. + generalize dependent t. simpl in *. + induction xs; simpl in *; intros; congruence. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v new file mode 100644 index 000000000..7e3c78dc2 --- /dev/null +++ b/test-suite/bugs/closed/4877.v @@ -0,0 +1,12 @@ +Ltac induction_last := + let v := match goal with + | |- forall x y, _ = _ -> _ => 1 + | |- forall x y, _ -> _ = _ -> _ => 2 + | |- forall x y, _ -> _ -> _ = _ -> _ => 3 + end in + induction v. + +Goal forall n m : nat, True -> n = m -> m = n. + induction_last. + reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v new file mode 100644 index 000000000..5569798d5 --- /dev/null +++ b/test-suite/bugs/closed/4880.v @@ -0,0 +1,11 @@ +Require Import Coq.Reals.Reals Coq.nsatz.Nsatz. +Local Open Scope R. + +Goal forall x y : R, + x*x = y * y -> + x*x = -y * -y -> + x*(x*x) = 0 -> (* The associativity does not actually matter, *) + (x*x)*x = 0. (* just otherwise [assumption] would solve the goal. *) +Proof. + nsatz. +Qed. diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v new file mode 100644 index 000000000..8c26af708 --- /dev/null +++ b/test-suite/bugs/closed/4882.v @@ -0,0 +1,50 @@ + +Definition Foo {T}{a : T} : T := a. + +Module A. + + Declare Implicit Tactic eauto. + + Goal forall A (x : A), A. + intros. + apply Foo. (* Check defined evars are normalized *) + (* Qed. *) + Abort. + +End A. + +Module B. + + Definition Foo {T}{a : T} : T := a. + + Declare Implicit Tactic eassumption. + + Goal forall A (x : A), A. + intros. + apply Foo. + (* Qed. *) + Abort. + +End B. + +Module C. + + Declare Implicit Tactic first [exact True|assumption]. + + Goal forall (x : True), True. + intros. + apply (@Foo _ _). + Qed. + +End C. + +Module D. + + Declare Implicit Tactic assumption. + + Goal forall A (x : A), A. + intros. + exact _. + Qed. + +End D. diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v new file mode 100644 index 000000000..9a35bcf95 --- /dev/null +++ b/test-suite/bugs/closed/4893.v @@ -0,0 +1,4 @@ +Goal True. +evar (P: Prop). +assert (H : P); [|subst P]; [exact I|]. +let T := type of H in not_evar T. diff --git a/test-suite/bugs/closed/4904.v b/test-suite/bugs/closed/4904.v new file mode 100644 index 000000000..a47c3b07a --- /dev/null +++ b/test-suite/bugs/closed/4904.v @@ -0,0 +1,11 @@ +Module A. +Module B. +Notation mynat := nat. +Notation nat := nat. +End B. +End A. + +Print A.B.nat. (* Notation A.B.nat := nat *) +Import A. +Print B.mynat. +Print B.nat. diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v new file mode 100644 index 000000000..219d532ac --- /dev/null +++ b/test-suite/bugs/closed/4932.v @@ -0,0 +1,44 @@ +(* Testing recursive notations with binders seen as terms *) + +Inductive ftele : Type := +| fb {T:Type} : T -> ftele +| fr {T} : (T -> ftele) -> ftele. + +Fixpoint args ftele : Type := + match ftele with + | fb _ => unit + | fr f => sigT (fun t => args (f t)) + end. + +Definition fpack := sigT args. +Definition pack fp fa : fpack := existT _ fp fa. + +Notation "'tele' x .. z := b" := + ( + (fun x => .. + (fun z => + pack + (fr (fun x => .. ( fr (fun z => fb b) ) .. ) ) + (existT _ x .. (existT _ z tt) .. ) + ) .. + ) + ) (at level 85, x binder, z binder). + +Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt)) + (existT _ (y,z) tt). + +Example test := tele (t : Type) := tt. +Example test' := test nat. +Print test. + +Example test2 := tele (t : Type) (x:t) := tt. +Example test2' := test2 nat 0. +Print test2. + +Example test3 := tele (t : Type) (y:=0) (x:t) := tt. +Example test3' := test3 nat 0. +Print test3. + +Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt. +Example test4' := test4 nat (1,2) 3. +Print test4. diff --git a/test-suite/bugs/closed/4955.v b/test-suite/bugs/closed/4955.v new file mode 100644 index 000000000..dce1f764c --- /dev/null +++ b/test-suite/bugs/closed/4955.v @@ -0,0 +1,98 @@ +(* An example involving a first-order unification triggering a cyclic constraint *) + +Module A. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) +: P y := + match p with eq_refl => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): p # (f +x) = f y + := match p with eq_refl => eq_refl end. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Delimit Scope functor_scope with functor. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C%category D%category} f%functor c%object : rename, simpl +nomatch. +Arguments morphism_of [C%category] [D%category] f%functor [s%object d%object] +m%morphism : rename, simpl nomatch. +Section path_functor. + Variable C : PreCategory. + Variable D : PreCategory. + + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G } + (only parsing). + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End A. + +(* A variant of it with more axioms *) + +Module B. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y). +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Axiom apD : forall {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y), p # (f +x) = f y. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C D} f c : rename, simpl nomatch. +Arguments morphism_of [C] [D] f [s d] m : rename, simpl nomatch. +Section path_functor. + Variable C D : PreCategory. + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G }. + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End B. diff --git a/test-suite/bugs/closed/4966.v b/test-suite/bugs/closed/4966.v new file mode 100644 index 000000000..bd93cdc85 --- /dev/null +++ b/test-suite/bugs/closed/4966.v @@ -0,0 +1,10 @@ +(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *) + +Axiom proof_admitted : False. +Hint Extern 0 => case proof_admitted : unused. +Ltac do_tac tac := tac. + +Goal False. + Set Ltac Profiling. + Fail solve [ do_tac auto ]. +Abort. diff --git a/test-suite/bugs/closed/4970.v b/test-suite/bugs/closed/4970.v new file mode 100644 index 000000000..7a896582f --- /dev/null +++ b/test-suite/bugs/closed/4970.v @@ -0,0 +1,3 @@ +(* Check "{{" is not confused with "{" in notations *) +Reserved Notation "x {{ y }}" (at level 40). +Notation "x {{ y }}" := (x y) (only parsing). diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v new file mode 100644 index 000000000..c3043ca5d --- /dev/null +++ b/test-suite/bugs/closed/5011.v @@ -0,0 +1,2 @@ +Record decoder (n : nat) W := { decode : W -> nat }. +Existing Class decoder. diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v new file mode 100644 index 000000000..12c958be6 --- /dev/null +++ b/test-suite/bugs/closed/5036.v @@ -0,0 +1,10 @@ +Section foo. + Context (F : Type -> Type). + Context (admit : forall {T}, F T = True). + Hint Rewrite (fun T => @admit T). + Lemma bad : F False. + Proof. + autorewrite with core. + constructor. + Qed. +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/5043.v b/test-suite/bugs/closed/5043.v new file mode 100644 index 000000000..4e6a0f878 --- /dev/null +++ b/test-suite/bugs/closed/5043.v @@ -0,0 +1,8 @@ +Unset Keep Admitted Variables. + +Section a. + Context (x : Type). + Definition foo : Type. + Admitted. +End a. +Check foo : Type. diff --git a/test-suite/bugs/closed/5045.v b/test-suite/bugs/closed/5045.v new file mode 100644 index 000000000..dc38738d8 --- /dev/null +++ b/test-suite/bugs/closed/5045.v @@ -0,0 +1,3 @@ +Axiom silly : 1 = 1 -> nat -> nat. +Goal forall pf : 1 = 1, silly pf 0 = 0 -> True. + Fail generalize (@eq nat). diff --git a/test-suite/bugs/closed/5065.v b/test-suite/bugs/closed/5065.v new file mode 100644 index 000000000..6bd677ba6 --- /dev/null +++ b/test-suite/bugs/closed/5065.v @@ -0,0 +1,6 @@ +Inductive foo := C1 : bar -> foo with bar := C2 : foo -> bar. + +Lemma L1 : foo -> True with L2 : bar -> True. +intros; clear L1 L2; abstract (exact I). +intros; exact I. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5066.v b/test-suite/bugs/closed/5066.v new file mode 100644 index 000000000..eed7f0f3f --- /dev/null +++ b/test-suite/bugs/closed/5066.v @@ -0,0 +1,7 @@ +Require Import Vector. + +Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) := + match v1 with + | nil _ => v2 + | cons _ e n' sv => vector_rev sv (cons A e n2 v2) + end. diff --git a/test-suite/bugs/closed/5077.v b/test-suite/bugs/closed/5077.v new file mode 100644 index 000000000..7e7f2c373 --- /dev/null +++ b/test-suite/bugs/closed/5077.v @@ -0,0 +1,8 @@ +(* Testing robustness of typing for a fixpoint with evars in its type *) + +Inductive foo (n : nat) : Type := . +Definition foo_denote {n} (x : foo n) : Type := match x with end. + +Definition baz : forall n (x : foo n), foo_denote x. +refine (fix go n (x : foo n) : foo_denote x := _). +Abort. diff --git a/test-suite/bugs/closed/5078.v b/test-suite/bugs/closed/5078.v new file mode 100644 index 000000000..ca73cbcc1 --- /dev/null +++ b/test-suite/bugs/closed/5078.v @@ -0,0 +1,5 @@ +(* Test coercion from ident to evaluable reference *) +Tactic Notation "unfold_hyp" hyp(H) := cbv delta [H]. +Goal True -> Type. + intro H''. + Fail unfold_hyp H''. diff --git a/test-suite/bugs/closed/5093.v b/test-suite/bugs/closed/5093.v new file mode 100644 index 000000000..3ded4dd30 --- /dev/null +++ b/test-suite/bugs/closed/5093.v @@ -0,0 +1,11 @@ +Axiom P : nat -> Prop. +Axiom PS : forall n, P n -> P (S n). +Axiom P0 : P 0. + +Hint Resolve PS : foobar. +Hint Resolve P0 : foobar. + +Goal P 100. +Proof. +Fail typeclasses eauto 100 with foobar. +typeclasses eauto 101 with foobar. diff --git a/test-suite/bugs/closed/5095.v b/test-suite/bugs/closed/5095.v new file mode 100644 index 000000000..b6f38e3e8 --- /dev/null +++ b/test-suite/bugs/closed/5095.v @@ -0,0 +1,5 @@ +(* Checking let-in abstraction *) +Goal let x := Set in let y := x in True. + intros x y. + (* There used to have a too strict dependency test there *) + set (s := Set) in (value of x). diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v new file mode 100644 index 000000000..20a537ab3 --- /dev/null +++ b/test-suite/bugs/closed/5096.v @@ -0,0 +1,219 @@ +Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List. + +Set Asymmetric Patterns. + +Notation eta x := (fst x, snd x). + +Inductive expr {var : Type} : Type := +| Const : expr +| LetIn : expr -> (var -> expr) -> expr. + +Definition Expr := forall var, @expr var. + +Fixpoint count_binders (e : @expr unit) : nat := +match e with +| LetIn _ eC => 1 + @count_binders (eC tt) +| _ => 0 +end. + +Definition CountBinders (e : Expr) : nat := count_binders (e _). + +Class Context (Name : Type) (var : Type) := + { ContextT : Type; + extendb : ContextT -> Name -> var -> ContextT; + empty : ContextT }. +Coercion ContextT : Context >-> Sortclass. +Arguments ContextT {_ _ _}, {_ _} _. +Arguments extendb {_ _ _} _ _ _. +Arguments empty {_ _ _}. + +Module Export Named. +Inductive expr Name : Type := +| Const : expr Name +| LetIn : Name -> expr Name -> expr Name -> expr Name. +End Named. + +Global Arguments Const {_}. +Global Arguments LetIn {_} _ _ _. + +Definition split_onames {Name : Type} (ls : list (option Name)) + : option (Name) * list (option Name) + := match ls with + | cons n ls' + => (n, ls') + | nil => (None, nil) + end. + +Section internal. + Context (InName OutName : Type) + {InContext : Context InName (OutName)} + {ReverseContext : Context OutName (InName)} + (InName_beq : InName -> InName -> bool). + + Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext) + (e : expr InName) (new_names : list (option OutName)) + : option (expr OutName) + := match e in Named.expr _ return option (expr _) with + | Const => Some Const + | LetIn n ex eC + => let '(n', new_names') := eta (split_onames new_names) in + match n', @register_reassign ctxi ctxr ex nil with + | Some n', Some x + => let ctxi := @extendb _ _ _ ctxi n n' in + let ctxr := @extendb _ _ _ ctxr n' n in + option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names') + | None, Some x + => let ctxi := ctxi in + @register_reassign ctxi ctxr eC new_names' + | _, None => None + end + end. + +End internal. + +Global Instance pos_context (var : Type) : Context positive var + := { ContextT := PositiveMap.t var; + extendb ctx key v := PositiveMap.add key v ctx; + empty := PositiveMap.empty _ }. + +Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _. + +Section language5. + Context (Name : Type). + + Local Notation expr := (@Top.expr Name). + Local Notation nexpr := (@Named.expr Name). + + Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e} + : option (nexpr) + := match e in @Top.expr _ return option (nexpr) with + | Top.Const => Some Named.Const + | Top.LetIn ex eC + => match @ocompile ex nil, split_onames ls with + | Some x, (Some n, ls')%core + => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls') + | _, _ => None + end + end. + + Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls). +End language5. + +Global Arguments compile {_} e ls. + +Fixpoint merge_liveness (ls1 ls2 : list unit) := + match ls1, ls2 with + | cons x xs, cons y ys => cons tt (@merge_liveness xs ys) + | nil, ls | ls, nil => ls + end. + +Section internal1. + Context (Name : Type) + (OutName : Type) + {Context : Context Name (list unit)}. + + Definition compute_livenessf_step + (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit) + (ctx : Context) + (e : expr Name) (prefix : list unit) + : list unit + := match e with + | Const => prefix + | LetIn n ex eC + => let lx := @compute_livenessf ctx ex prefix in + let lx := merge_liveness lx (prefix ++ repeat tt 1) in + let ctx := @extendb _ _ _ ctx n (lx) in + @compute_livenessf ctx eC (prefix ++ repeat tt 1) + end. + + Fixpoint compute_liveness ctx e prefix + := @compute_livenessf_step (@compute_liveness) ctx e prefix. + + Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName) + : list (option OutName) + := match ls with + | nil => nil + | cons live xs + => match lsn with + | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn' + | nil => def :: @insert_dead_names_gen def xs nil + end + end. + Definition insert_dead_names def (e : expr Name) + := insert_dead_names_gen def (compute_liveness empty e nil). +End internal1. + +Global Arguments insert_dead_names {_ _ _} def e lsn. + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. + +Section language7. + Context {Context : Context unit (positive)}. + + Local Notation nexpr := (@Named.expr unit). + + Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit) + : option (nexpr) + := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in + match e with + | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *) + (fun names => register_reassign empty empty e names) + | None => None + end. +End language7. + +Global Arguments CompileAndEliminateDeadCode {_} e ls. + +Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var + := {| ContextT := Ctx; + extendb ctx n v := extendb ctx (f n) v; + empty := empty |}. + +Definition Register := Datatypes.unit. + +Global Instance RegisterContext {var : Type} : Context Register var + := ContextOn (fun _ => 1%positive) (pos_context var). + +Definition syntax := Named.expr Register. + +Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls) + := match res return match res with None => _ | _ => _ end with + | Some v => v + | None => I + end. + +Definition dummy_registers (n : nat) : list Register + := List.map (fun _ => tt) (seq 0 n). +Definition DefaultRegisters (e : Expr) : list Register + := dummy_registers (CountBinders e). + +Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e). + +Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200). +Notation "#[ var ]#" := (@Top.Const var). + +Definition compiled_syntax : Expr := fun (var : Type) => +( + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + @Top.Const var). + +Definition v := + Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)). + +Timeout 2 Eval vm_compute in v. diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v new file mode 100644 index 000000000..37b239cf6 --- /dev/null +++ b/test-suite/bugs/closed/5097.v @@ -0,0 +1,7 @@ +(* Tracing existing evars along the weakening rule ("clear") *) +Goal forall y, exists x, x=0->x=y. +intros. +eexists ?[x]. +intros. +let x:=constr:(ltac:(clear y; exact 0)) in idtac x. +Abort. diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v new file mode 100644 index 000000000..bcde510ee --- /dev/null +++ b/test-suite/bugs/closed/5123.v @@ -0,0 +1,33 @@ +(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *) + +(*Pose an open constr to prevent immediate typeclass resolution in holes:*) +Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H. + +Inductive vect A : nat -> Type := +| vnil : vect A 0 +| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n). + +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Require Bool. + +Instance Bool_eqdec : Eqdec bool := Bool.bool_dec. + +Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}. + +Typeclasses eauto := debug. + +Goal True. + unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. + all:cycle 2. + eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. +Abort. + +Goal True. + opose (@vect_sigT_eqdec _ _ _ _) as H. + Unshelve. + all:cycle 3. + eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. +Abort.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v new file mode 100644 index 000000000..831e8fb50 --- /dev/null +++ b/test-suite/bugs/closed/5127.v @@ -0,0 +1,15 @@ +Fixpoint arrow (n: nat) := + match n with + | S n => bool -> arrow n + | O => bool + end. + +Fixpoint apply (n : nat) : arrow n -> bool := + match n return arrow n -> bool with + | S n => fun f => apply _ (f true) + | O => fun x => x + end. + +Axiom f : arrow 10000. +Definition v : bool := Eval compute in apply _ f. +Definition w : bool := Eval vm_compute in v. diff --git a/test-suite/bugs/closed/5145.v b/test-suite/bugs/closed/5145.v new file mode 100644 index 000000000..0533d21e0 --- /dev/null +++ b/test-suite/bugs/closed/5145.v @@ -0,0 +1,10 @@ +Class instructions := + { + W : Type; + ldi : nat -> W + }. + +Fail Definition foo := + let y2 := ldi 0 in + let '(CF, _) := (true, 0) in + y2. diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v new file mode 100644 index 000000000..684dba196 --- /dev/null +++ b/test-suite/bugs/closed/5149.v @@ -0,0 +1,47 @@ +Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x. +intros. +eexists. +rewrite <- H. +eassumption. +Qed. + +Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) + (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : +flat_type -> Type) + (v v' : interp_flat_type1 t'), + v = v' -> + forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0) + (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> +interp_flat_type0 t0) + (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t)) + (x' : interp_flat_type1 (Tbase t)) (T : Type) + (flatten_binding_list : forall t0 : flat_type, + interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T) + (P : T -> list T -> Prop) (prod : Type -> Type -> Type) + (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) +(interp_flat_type1 (Tbase x0)) -> T) + (pair : forall A B : Type, A -> B -> prod A B), + P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x')) + (flatten_binding_list t' (SmartVarVar t' v') v) -> + (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 +t'0) + (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)), + P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 +x'0)) + (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf +(Tbase t0) x0 = x'0) -> + interpf (Tbase t) x = x'. +Proof. + intros ?????????????????????? interpf_SmartVarVar. + solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail +"too early". + Undo. + (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) + Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ]. + solve [eapply interpf_SmartVarVar; subst; eassumption]. + Undo. + Unset Solve Unification Constraints. + (* User control of when constraints are solved *) + solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ]. +Qed. + diff --git a/test-suite/bugs/closed/5161.v b/test-suite/bugs/closed/5161.v new file mode 100644 index 000000000..d28303b8a --- /dev/null +++ b/test-suite/bugs/closed/5161.v @@ -0,0 +1,27 @@ +(* Check that the presence of binders with type annotation do not + prevent the recursive binder part to be found *) + +From Coq Require Import Utf8. + +Delimit Scope C_scope with C. +Global Open Scope C_scope. + +Delimit Scope uPred_scope with I. + +Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x. + +Notation "∀ x .. y , P" := + (FORALL (λ x, .. (FORALL (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. +Infix "∧" := and : uPred_scope. + +(* The next command fails with + In recursive notation with binders, Φ is expected to come without type. + I would expect this notation to work fine, since the ∀ does support + type annotation. +*) +Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := + (∀ Φ : _ → _, + (∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I + (at level 20, x closed binder, y closed binder, + format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope. diff --git a/test-suite/bugs/closed/5181.v b/test-suite/bugs/closed/5181.v new file mode 100644 index 000000000..0e6d47197 --- /dev/null +++ b/test-suite/bugs/closed/5181.v @@ -0,0 +1,3 @@ +Definition foo (x y : nat) := x. +Fail Arguments foo {_} : assert. + diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v new file mode 100644 index 000000000..7254afb42 --- /dev/null +++ b/test-suite/bugs/closed/5198.v @@ -0,0 +1,39 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *) +(* File reduced by coq-bug-finder from original input, then from 286 lines to +27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, +then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from +253 lines to 65 lines, then from 79 lines to 65 lines *) +(* coqc version 8.6.0 (November 2016) compiled on Nov 12 2016 14:43:52 with +OCaml 4.02.3 + coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-v8.6,v8.6 +(7e992fa784ee6fa48af8a2e461385c094985587d) *) +Axiom admit : forall {T}, T. +Set Printing Implicit. +Inductive nat := O | S (_ : nat). +Axiom f : forall (_ _ : nat), nat. +Class ZLikeOps (e : nat) + := { LargeT : Type ; SmallT : Type ; CarryAdd : forall (_ _ : LargeT), LargeT +}. +Class BarrettParameters := + { b : nat ; k : nat ; ops : ZLikeOps (f b k) }. +Axiom barrett_reduce_function_bundled : forall {params : BarrettParameters} + (_ : @LargeT _ (@ops params)), + @SmallT _ (@ops params). + +Global Instance ZZLikeOps e : ZLikeOps (f (S O) e) + := { LargeT := nat ; SmallT := nat ; CarryAdd x y := y }. +Definition SRep := nat. +Local Instance x86_25519_Barrett : BarrettParameters + := { b := S O ; k := O ; ops := ZZLikeOps O }. +Definition SRepAdd : forall (_ _ : SRep), SRep + := let v := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)) in + v. +Definition SRepAdd' : forall (_ _ : SRep), SRep + := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)). +(* Error: +In environment +x : SRep +y : SRep +The term "x" has type "SRep" while it is expected to have type + "@LargeT ?e ?ZLikeOps". + *) diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v new file mode 100644 index 000000000..ed137395f --- /dev/null +++ b/test-suite/bugs/closed/5203.v @@ -0,0 +1,5 @@ +Goal True. + Typeclasses eauto := debug. + Fail solve [ typeclasses eauto ]. + Fail typeclasses eauto. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 008fb72c4..73da464bb 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -22,8 +22,8 @@ Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := o Ltac present_obj from to := match goal with - | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * - | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * + | [ _ : context[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * + | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * end. Section NaturalTransformationComposition. diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v index 5e5d5ab3e..3d16e7ac0 100644 --- a/test-suite/bugs/closed/HoTT_coq_058.v +++ b/test-suite/bugs/closed/HoTT_coq_058.v @@ -95,10 +95,10 @@ Goal forall (T : Type) (T0 : T -> T -> Type) | tt => idpath end)) (x1; p) = (x1; p). intros. -let F := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in -let H := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in -let X := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in -let T := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in +let F := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in +let H := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in +let X := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in +let T := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in let t0 := fresh "t0" in let t1 := fresh "t1" in let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in @@ -116,7 +116,7 @@ let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in let GL1' := fresh in set (GL0' := GL0); - let arg := match GL0 with appcontext[x0 ?arg] => constr:(arg) end in + let arg := match GL0 with context[x0 ?arg] => constr:(arg) end in assert (t1 = arg) by (subst t1; reflexivity); subst t1; pattern (x0 arg) in GL0'; match goal with diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v index 5fbcfef4e..de60fd0ae 100644 --- a/test-suite/bugs/closed/HoTT_coq_117.v +++ b/test-suite/bugs/closed/HoTT_coq_117.v @@ -16,10 +16,29 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, Admitted. Inductive Empty : Set := . -Instance contr_from_Empty {_ : Funext} (A : Type) : +Fail Instance contr_from_Empty {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect _ x)). + +Fail Instance contr_from_Empty {F : Funext} (A : Type) : Contr_internal (Empty -> A) := BuildContr _ (Empty_rect (fun _ => A)) (fun f => path_forall _ f (fun x => Empty_rect _ x)). + +(** This could be disallowed, this uses the Funext argument *) +Instance contr_from_Empty {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)). + +Instance contr_from_Empty' {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)). (* Toplevel input, characters 15-220: Anomaly: unknown meta ?190. Please report. *) diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/bugs/closed/PLACEHOLDER.v diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v new file mode 100644 index 000000000..5838dcd8a --- /dev/null +++ b/test-suite/bugs/closed/bug_4836.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *) diff --git a/test-suite/bugs/closed/bug_4836/PLACEHOLDER b/test-suite/bugs/closed/bug_4836/PLACEHOLDER new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/bugs/closed/bug_4836/PLACEHOLDER |