diff options
Diffstat (limited to 'test-suite')
26 files changed, 543 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 59cc3e5a38..0935617fbf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -112,7 +112,7 @@ INTERACTIVE := interactive UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc ssr primitive/uint63 primitive/float ltac2 + coqdoc ssr $(wildcard primitive/*) ltac2 # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS) diff --git a/test-suite/bugs/closed/bug_11121.v b/test-suite/bugs/closed/bug_11121.v new file mode 100644 index 0000000000..6112a443ab --- /dev/null +++ b/test-suite/bugs/closed/bug_11121.v @@ -0,0 +1,21 @@ +Declare Custom Entry example. + +Module M1. +Fixpoint stupid (x : nat) : nat := 1. +Reserved Notation " x '==' 1 " (in custom example at level 0, x constr). +Notation " x '==' 1" := (stupid x) (in custom example). +End M1. + +Module M2. +Fixpoint stupid (x : nat) : nat := 1. +Notation " x '==' 1" := (stupid x) (in custom example at level 0). +Fail Notation " x '==' 1" := (stupid x) (in custom example at level 1). +End M2. + +Module M3. +Reserved Notation " x '==' 1 " (in custom example at level 55, x constr). + +Fixpoint stupid (x : nat) : nat := 1 +where " x '==' 1" := (stupid x) (in custom example). + +End M3. diff --git a/test-suite/bugs/closed/bug_12528.v b/test-suite/bugs/closed/bug_12528.v new file mode 100644 index 0000000000..4ab05ac9b8 --- /dev/null +++ b/test-suite/bugs/closed/bug_12528.v @@ -0,0 +1,6 @@ +Set Primitive Projections. +Set Universe Polymorphism. +Record ptd := Ptd { t : Type ; p : t }. +Definition type := Ptd Type (unit:Type). +Definition type' := Ptd Type (p type). +Canonical type'. diff --git a/test-suite/bugs/closed/bug_12551.v b/test-suite/bugs/closed/bug_12551.v new file mode 100644 index 0000000000..77ecb367ec --- /dev/null +++ b/test-suite/bugs/closed/bug_12551.v @@ -0,0 +1,8 @@ + +Section S. + Context [A:Type] (a:A). + Definition id := a. +End S. + +Check id : forall A, A -> A. +Check id 0 : nat. diff --git a/test-suite/bugs/closed/bug_12649.v b/test-suite/bugs/closed/bug_12649.v new file mode 100644 index 0000000000..5547de84ff --- /dev/null +++ b/test-suite/bugs/closed/bug_12649.v @@ -0,0 +1,11 @@ + + +Module Type A. + + Record baz : Prop := B { }. (* any sort would do *) + +End A. + +Print A. +Module Type UseA (c: A). End UseA. +Print UseA. (* ANOMALY! Int.Map.get's assert false *) diff --git a/test-suite/bugs/closed/bug_12651.v b/test-suite/bugs/closed/bug_12651.v new file mode 100644 index 0000000000..cdeeb84912 --- /dev/null +++ b/test-suite/bugs/closed/bug_12651.v @@ -0,0 +1,6 @@ + +Set Warnings "+implicits-in-term". +Definition thing1 : forall {A}, A -> A := fun A a => a. +Check thing1 : _ -> _. +Fail Definition thing2 : forall {A}, A -> A := fun [A] a => a. +Fail Definition thing2 : forall A, A -> A := fun {A} a => a. diff --git a/test-suite/failure/uip_loop.v b/test-suite/failure/uip_loop.v new file mode 100644 index 0000000000..5b4a88e7cc --- /dev/null +++ b/test-suite/failure/uip_loop.v @@ -0,0 +1,24 @@ +Set Definitional UIP. + +Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. +Arguments srefl {_ _}. + +(* Axiom implied by propext (so consistent) *) +Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q. + +Definition transport (P Q:Prop) (x:P) (y:Q) : Q + := match all_eq P Q x y with srefl => x end. + +Definition top : Prop := forall P : Prop, P -> P. + +Definition c : top := + fun P p => + transport + (top -> top) + P + (fun x : top => x (top -> top) (fun x => x) x) + p. + +Fail Timeout 1 Eval lazy in c (top -> top) (fun x => x) c. +(* loops *) diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v index 018596ed95..8c06bff056 100644 --- a/test-suite/ltac2/constr.v +++ b/test-suite/ltac2/constr.v @@ -10,3 +10,9 @@ Axiom something : SProp. Ltac2 Eval match (kind '(forall x : something, bool)) with | Prod a c => a | _ => throw Match_failure end. + +From Coq Require Import Int63 PArray. +Open Scope array_scope. +Ltac2 Eval match (kind '([|true|true|])) with + | Array _ _ _ ty => ty + | _ => throw Match_failure end. diff --git a/test-suite/ltac2/syntax.v b/test-suite/ltac2/syntax.v new file mode 100644 index 0000000000..872b2142d0 --- /dev/null +++ b/test-suite/ltac2/syntax.v @@ -0,0 +1,12 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Type ('a, 'b, 'c) t. +Ltac2 Type ('a) u. +Ltac2 Type 'a v. + +Ltac2 foo + (f : ('a, 'b, 'c) t -> ('a -> 'a, 'b -> 'c, 'c * 'c) t) + (x : ('a, 'b, 'c) t) := + f x. + +Ltac2 bar (x : 'a u) (y : ('b) v) := x. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ca4858d7a7..ba316ceb64 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,6 +7,8 @@ bli : Type Axioms: bli : Type Axioms: +@seq relies on definitional UIP. +Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index 4c980fddba..71e642519c 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -45,6 +45,32 @@ Module Poly. End Poly. +Module UIP. + Set Definitional UIP. + + Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. + Arguments srefl {_ _}. + + Definition eq_to_seq {A x y} (e:x = y :> A) : seq x y + := match e with eq_refl => srefl end. + Definition seq_to_eq {A x y} (e:seq x y) : x = y :> A + := match e with srefl => eq_refl end. + + Definition norm {A x y} (e:x = y :> A) : x = y + := seq_to_eq (eq_to_seq e). + + Definition norm_id {A x y} (e:x = y :> A) : norm e = e + := match e with eq_refl => eq_refl end. + + Theorem UIP {A x y} (e e':x = y :> A) : e = e'. + Proof. + rewrite <-(norm_id e), <-(norm_id e'). + reflexivity. + Defined. + + Print Assumptions UIP. +End UIP. (* The original test-case of the bug-report *) diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 317e9c3757..09feca71e7 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -455,3 +455,6 @@ PreOrder_Reflexive: reflexive_eq_dom_reflexive: forall {A B : Type} {R' : Relation_Definitions.relation B}, Reflexive R' -> Reflexive (eq ==> R')%signature +B.b: B.a +A.b: A.a +F.L: F.P 0 diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 4ec7a760b9..a5ac2cb511 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -66,3 +66,26 @@ Reset Initial. Require Import Morphisms. Search is:Instance [ Reflexive | Symmetric ]. + +Module Bug12525. + (* This was revealing a kernel bug with delta-resolution *) + Module A. Axiom a:Prop. Axiom b:a. End A. + Module B. Include A. End B. + Module M. + Search B.a. + End M. +End Bug12525. + +From Coq Require Lia. + +Module Bug12647. + (* Similar to #12525 *) + Module Type Foo. + Axiom P : nat -> Prop. + Axiom L : P 0. + End Foo. + + Module Bar (F : Foo). + Search F.P. + End Bar. +End Bug12647. diff --git a/test-suite/primitive/arrays/copy.v b/test-suite/primitive/arrays/copy.v new file mode 100644 index 0000000000..bc8e733334 --- /dev/null +++ b/test-suite/primitive/arrays/copy.v @@ -0,0 +1,22 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t : array nat := [| 1; 5; 2 | 4 |]. +Definition t' : array nat := PArray.copy t. + +Definition foo1 := (eq_refl : t'.[1] = 5). +Definition foo2 := (eq_refl 5 <: t'.[1] = 5). +Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). +Definition x1 := Eval compute in t'.[1]. +Definition foo4 := (eq_refl : x1 = 5). +Definition x2 := Eval cbn in t'.[1]. +Definition foo5 := (eq_refl : x2 = 5). + +Definition foo6 := (eq_refl : t.[1] = 5). +Definition foo7 := (eq_refl 5 <: t.[1] = 5). +Definition foo8 := (eq_refl 5 <<: t.[1] = 5). +Definition x3 := Eval compute in t.[1]. +Definition foo9 := (eq_refl : x3 = 5). +Definition x4 := Eval cbn in t.[1]. +Definition foo10 := (eq_refl : x4 = 5). diff --git a/test-suite/primitive/arrays/default.v b/test-suite/primitive/arrays/default.v new file mode 100644 index 0000000000..3b89787faf --- /dev/null +++ b/test-suite/primitive/arrays/default.v @@ -0,0 +1,10 @@ +From Coq Require Import Int63 PArray. + +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition foo1 := (eq_refl : default t = 4). +Definition foo2 := (eq_refl 4 <: default t = 4). +Definition foo3 := (eq_refl 4 <<: default t = 4). +Definition x1 := Eval compute in default t. +Definition foo4 := (eq_refl : x1 = 4). +Definition x2 := Eval cbn in default t. +Definition foo5 := (eq_refl : x2 = 4). diff --git a/test-suite/primitive/arrays/get.v b/test-suite/primitive/arrays/get.v new file mode 100644 index 0000000000..9a6f09a83b --- /dev/null +++ b/test-suite/primitive/arrays/get.v @@ -0,0 +1,86 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +(* Test reduction of primitives on array with kernel conversion, vm_compute, +native_compute, cbv, cbn *) + +(* Immediate values *) +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition foo1 := (eq_refl : t.[0] = 1). +Definition foo2 := (eq_refl 1 <: t.[0] = 1). +Definition foo3 := (eq_refl 1 <<: t.[0] = 1). +Definition x1 := Eval compute in t.[0]. +Definition foo4 := (eq_refl : x1 = 1). +Definition x2 := Eval cbn in t.[0]. +Definition foo5 := (eq_refl : x2 = 1). + +Definition foo6 := (eq_refl : t.[2] = 2). +Definition foo7 := (eq_refl 2 <: t.[2] = 2). +Definition foo8 := (eq_refl 2 <<: t.[2] = 2). +Definition x3 := Eval compute in t.[2]. +Definition foo9 := (eq_refl : x3 = 2). +Definition x4 := Eval cbn in t.[2]. +Definition foo10 := (eq_refl : x4 = 2). + +Definition foo11 := (eq_refl : t.[99] = 4). +Definition foo12 := (eq_refl 4 <: t.[99] = 4). +Definition foo13 := (eq_refl 4 <<: t.[99] = 4). +Definition x5 := Eval compute in t.[4]. +Definition foo14 := (eq_refl : x5 = 4). +Definition x6 := Eval cbn in t.[4]. +Definition foo15 := (eq_refl : x6 = 4). + +(* Computations inside the array *) +Definition t2 : array nat := [| 1 + 3 | 5 |]. +Definition foo16 := (eq_refl : t2.[0] = 4). +Definition foo17 := (eq_refl 4 <: t2.[0] = 4). +Definition foo18 := (eq_refl 4 <<: t2.[0] = 4). +Definition x7 := Eval compute in t2.[0]. +Definition foo19 := (eq_refl : x7 = 4). +Definition x8 := Eval cbn in t2.[0]. +Definition foo20 := (eq_refl : x8 = 4). + +(* Functions inside the array *) +Definition t3 : array (nat -> nat) := [| fun x => x | fun x => O |]. +Definition foo21 := (eq_refl : t3.[0] 2 = 2). +Definition foo22 := (eq_refl 2 <: t3.[0] 2 = 2). +Definition foo23 := (eq_refl 2 <<: t3.[0] 2 = 2). +Definition x9 := Eval compute in t3.[0] 2. +Definition foo24 := (eq_refl : x9 = 2). +Definition x10 := Eval cbn in t3.[0] 2. +Definition foo25 := (eq_refl : x10 = 2). + +Ltac check_const_eq name constr := + let v := (eval cbv delta [name] in name) in + tryif constr_eq v constr + then idtac + else fail 0 "Not syntactically equal:" name ":=" v "<>" constr. + +Notation check_const_eq name constr := (ltac:(check_const_eq name constr; exact constr)) (only parsing). + +(* Stuck primitive *) +Definition lazy_stuck_get := Eval lazy in (fun A (t : array A) => t.[0]). +Definition vm_stuck_get := Eval vm_compute in (fun A (t : array A) => t.[0]). +Definition native_stuck_get := Eval native_compute in (fun A (t : array A) => t.[0]). +Definition compute_stuck_get := Eval compute in (fun A (t : array A) => t.[0]). +Definition cbn_stuck_get := Eval cbn in (fun A (t : array A) => t.[0]). + +Check check_const_eq lazy_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq vm_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq native_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq compute_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq cbn_stuck_get (fun A (t : array A) => t.[0]). + +(* Under-application *) +Definition lazy_get := Eval lazy in @PArray.get. +Definition vm_get := Eval vm_compute in @PArray.get. +Definition native_get := Eval native_compute in @PArray.get. +Definition compute_get := Eval compute in @PArray.get. +Definition cbn_get := Eval cbn in @PArray.get. + +Check check_const_eq lazy_get (@PArray.get). +Check check_const_eq vm_get (fun A (t : array A) i => t.[i]). +Check check_const_eq native_get (fun A (t : array A) i => t.[i]). +Check check_const_eq compute_get (@PArray.get). +Check check_const_eq cbn_get (@PArray.get). diff --git a/test-suite/primitive/arrays/length.v b/test-suite/primitive/arrays/length.v new file mode 100644 index 0000000000..67f686f2fb --- /dev/null +++ b/test-suite/primitive/arrays/length.v @@ -0,0 +1,12 @@ +From Coq Require Import Int63 PArray. + +Open Scope int63_scope. + +Definition t : array nat := [| 1; 3; 2 | 4 |]%nat. +Definition foo1 := (eq_refl : PArray.length t = 3). +Definition foo2 := (eq_refl 3 <: PArray.length t = 3). +Definition foo3 := (eq_refl 3 <<: PArray.length t = 3). +Definition x1 := Eval compute in PArray.length t. +Definition foo4 := (eq_refl : x1 = 3). +Definition x2 := Eval cbn in PArray.length t. +Definition foo5 := (eq_refl : x2 = 3). diff --git a/test-suite/primitive/arrays/literal.v b/test-suite/primitive/arrays/literal.v new file mode 100644 index 0000000000..13e57adbbe --- /dev/null +++ b/test-suite/primitive/arrays/literal.v @@ -0,0 +1,6 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |]. +Definition t2 := [|Type|Type|]. diff --git a/test-suite/primitive/arrays/make.v b/test-suite/primitive/arrays/make.v new file mode 100644 index 0000000000..a3a39470ed --- /dev/null +++ b/test-suite/primitive/arrays/make.v @@ -0,0 +1,18 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +(* Immediate values *) +Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |]. +Definition t2 := PArray.make 4 3. +Definition foo1 := (eq_refl : t1 = t2). +Definition foo2 := (eq_refl t1 <: t1 = t2). +Definition foo3 := (eq_refl t1 <<: t1 = t2). +Definition x1 := Eval compute in t2. +Definition foo4 := (eq_refl : x1 = t1). +Definition x2 := Eval cbn in t2. +Definition foo5 := (eq_refl : x2 = t1). + +Definition partial1 := Eval lazy in @PArray.make. +Definition partial2 := Eval vm_compute in @PArray.make. +Definition partial3 := Eval native_compute in @PArray.make. diff --git a/test-suite/primitive/arrays/max_length.v b/test-suite/primitive/arrays/max_length.v new file mode 100644 index 0000000000..54a6af7a19 --- /dev/null +++ b/test-suite/primitive/arrays/max_length.v @@ -0,0 +1,13 @@ +From Coq Require Import Int63 PArray. + +Open Scope int63_scope. + +Definition max_length := 4194303. + +Definition foo1 := (eq_refl max_length : PArray.max_length = max_length). +Definition foo2 := (eq_refl max_length <: PArray.max_length = max_length). +Definition foo3 := (eq_refl max_length <<: PArray.max_length = max_length). +Definition max_length2 := Eval compute in PArray.max_length. +Definition foo4 := (eq_refl : max_length = max_length2). +Definition max_length3 := Eval cbn in PArray.max_length. +Definition foo5 := (eq_refl : max_length = max_length3). diff --git a/test-suite/primitive/arrays/nested.v b/test-suite/primitive/arrays/nested.v new file mode 100644 index 0000000000..841cee4463 --- /dev/null +++ b/test-suite/primitive/arrays/nested.v @@ -0,0 +1,47 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Module OneLevel. + +Inductive foo : Set := + C : array foo -> foo. + +Fixpoint f1 (x : foo) {struct x} : False := + match x with + | C t => f1 (t.[0]) + end. + +Fixpoint f2 (x : foo) {struct x} : False := + f2 match x with + | C t => t.[0] + end. + +Fixpoint f3 (x : foo) {struct x} : False := + match x with + | C t => f3 (PArray.default t) + end. + +End OneLevel. + +Module TwoLevels. + +Inductive foo : Set := + C : array (array foo) -> foo. + +Fixpoint f1 (x : foo) {struct x} : False := + match x with + | C t => f1 (t.[0].[0]) + end. + +Fixpoint f2 (x : foo) {struct x} : False := + f2 match x with + | C t => t.[0].[0] + end. + +Fixpoint f3 (x : foo) {struct x} : False := + match x with + | C t => f3 (PArray.default (PArray.default t)) + end. + +End TwoLevels. diff --git a/test-suite/primitive/arrays/reroot.v b/test-suite/primitive/arrays/reroot.v new file mode 100644 index 0000000000..172a118cc7 --- /dev/null +++ b/test-suite/primitive/arrays/reroot.v @@ -0,0 +1,22 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t : array nat := [| 1; 5; 2 | 4 |]. +Definition t' : array nat := PArray.reroot t. + +Definition foo1 := (eq_refl : t'.[1] = 5). +Definition foo2 := (eq_refl 5 <: t'.[1] = 5). +Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). +Definition x1 := Eval compute in t'.[1]. +Definition foo4 := (eq_refl : x1 = 5). +Definition x2 := Eval cbn in t'.[1]. +Definition foo5 := (eq_refl : x2 = 5). + +Definition foo6 := (eq_refl : t.[1] = 5). +Definition foo7 := (eq_refl 5 <: t.[1] = 5). +Definition foo8 := (eq_refl 5 <<: t.[1] = 5). +Definition x3 := Eval compute in t.[1]. +Definition foo9 := (eq_refl : x3 = 5). +Definition x4 := Eval cbn in t.[1]. +Definition foo10 := (eq_refl : x4 = 5). diff --git a/test-suite/primitive/arrays/set.v b/test-suite/primitive/arrays/set.v new file mode 100644 index 0000000000..f265c37ea8 --- /dev/null +++ b/test-suite/primitive/arrays/set.v @@ -0,0 +1,22 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition t' : array nat := t.[1 <- 5]. + +Definition foo1 := (eq_refl : t'.[1] = 5). +Definition foo2 := (eq_refl 5 <: t'.[1] = 5). +Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). +Definition x1 := Eval compute in t'.[1]. +Definition foo4 := (eq_refl : x1 = 5). +Definition x2 := Eval cbn in t'.[1]. +Definition foo5 := (eq_refl : x2 = 5). + +Definition foo6 := (eq_refl : t.[1] = 3). +Definition foo7 := (eq_refl 3 <: t.[1] = 3). +Definition foo8 := (eq_refl 3 <<: t.[1] = 3). +Definition x3 := Eval compute in t.[1]. +Definition foo9 := (eq_refl : x3 = 3). +Definition x4 := Eval cbn in t.[1]. +Definition foo10 := (eq_refl : x4 = 3). diff --git a/test-suite/success/bug_10890.v b/test-suite/success/bug_10890.v new file mode 100644 index 0000000000..37b6c816cc --- /dev/null +++ b/test-suite/success/bug_10890.v @@ -0,0 +1,8 @@ +Require Import Derive. + +Derive foo SuchThat (foo = foo :> nat) As bar. +Proof. + Unshelve. + 2:abstract exact 0. + exact eq_refl. +Defined. (* or Qed: anomaly kernel doesn't support existential variables *) diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v index 268c1880d2..d3e2749088 100644 --- a/test-suite/success/sprop.v +++ b/test-suite/success/sprop.v @@ -112,6 +112,7 @@ Inductive Istrue : bool -> SProp := istrue : Istrue true. Definition Istrue_sym (b:bool) := if b then sUnit else sEmpty. Definition Istrue_to_sym b (i:Istrue b) : Istrue_sym b := match i with istrue => stt end. +(* We don't need primitive elimination to relevant types for this *) Definition Istrue_rec (P:forall b, Istrue b -> Set) (H:P true istrue) b (i:Istrue b) : P b i. Proof. destruct b. diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v new file mode 100644 index 0000000000..eae1b75689 --- /dev/null +++ b/test-suite/success/sprop_uip.v @@ -0,0 +1,127 @@ + +Set Allow StrictProp. +Set Definitional UIP. + +Set Warnings "+bad-relevance". + +(** Case inversion, conversion and universe polymorphism. *) +Set Universe Polymorphism. +Inductive IsTy@{i j} : Type@{j} -> SProp := + isty : IsTy Type@{i}. + +Definition IsTy_rec_red@{i j+} (P:forall T : Type@{j}, IsTy@{i j} T -> Set) + v (e:IsTy@{i j} Type@{i}) + : IsTy_rec P v _ e = v + := eq_refl. + + +(** Identity! Currently we have UIP. *) +Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. + +Definition transport {A} (P:A -> Type) {x y} (e:seq x y) (v:P x) : P y := + match e with + srefl _ => v + end. + +Definition transport_refl {A} (P:A -> Type) {x} (e:seq x x) v + : transport P e v = v + := @eq_refl (P x) v. + +Definition id_unit (x : unit) := x. +Definition transport_refl_id {A} (P : A -> Type) {x : A} (u : P x) + : P (transport (fun _ => A) (srefl _ : seq (id_unit tt) tt) x) + := u. + +(** We don't ALWAYS reduce (this uses a constant transport so that the + equation is well-typed) *) +Fail Definition transport_block A B (x y:A) (e:seq x y) v + : transport (fun _ => B) e v = v + := @eq_refl B v. + +Inductive sBox (A:SProp) : Prop + := sbox : A -> sBox A. + +Definition transport_refl_box (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v + : transport P e v = v + := eq_refl. + +(** TODO? add tests for binders which aren't lambda. *) +Definition transport_box := + Eval lazy in (fun (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v => + transport P e v). + +Lemma transport_box_ok : transport_box = fun A P x y e v => v. +Proof. + unfold transport_box. + match goal with |- ?x = ?x => reflexivity end. +Qed. + +(** Play with UIP *) +Lemma of_seq {A:Type} {x y:A} (p:seq x y) : x = y. +Proof. + destruct p. reflexivity. +Defined. + +Lemma to_seq {A:Type} {x y:A} (p: x = y) : seq x y. +Proof. + destruct p. reflexivity. +Defined. + +Lemma eq_srec (A:Type) (x y:A) (P:x=y->Type) : (forall e : seq x y, P (of_seq e)) -> forall e, P e. +Proof. + intros H e. destruct e. + apply (H (srefl _)). +Defined. + +Lemma K : forall {A x} (p:x=x:>A), p = eq_refl. +Proof. + intros A x. apply eq_srec. intros;reflexivity. +Defined. + +Definition K_refl : forall {A x}, @K A x eq_refl = eq_refl + := fun A x => eq_refl. + +Section funext. + + Variable sfunext : forall {A B} (f g : A -> B), (forall x, seq (f x) (g x)) -> seq f g. + + Lemma funext {A B} (f g : A -> B) (H:forall x, (f x) = (g x)) : f = g. + Proof. + apply of_seq,sfunext;intros x;apply to_seq,H. + Defined. + + Definition funext_refl A B (f : A -> B) : funext f f (fun x => eq_refl) = eq_refl + := eq_refl. +End funext. + +(* test reductions on inverted cases *) + +(* first check production of correct blocked cases *) +Definition lazy_seq_rect := Eval lazy in seq_rect. +Definition vseq_rect := Eval vm_compute in seq_rect. +Definition native_seq_rect := Eval native_compute in seq_rect. +Definition cbv_seq_rect := Eval cbv in seq_rect. + +(* check it reduces according to indices *) +Ltac reset := match goal with H : _ |- _ => change (match H with srefl _ => False end) end. +Ltac check := match goal with |- False => idtac end. +Lemma foo (H:seq 0 0) : False. +Proof. + reset. + Fail check. (* check that "reset" and "check" actually do something *) + + lazy; check; reset. + + (* TODO *) + vm_compute. Fail check. + native_compute. Fail check. + cbv. Fail check. + cbn. Fail check. + simpl. Fail check. +Abort. + +(* check that extraction doesn't fall apart on matches with special reduction *) +Require Extraction. + +Extraction seq_rect. |