blob: 583ef0ef3bf1619eb2494efbb6b85cc423117a89 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
Require Import Coq.Program.Program.
(* Set Universe Polymorphism. *)
Set Printing Universes.
Axiom ALL : forall {T:Prop}, T.
Inductive Expr : Set := E (a : Expr).
Parameter Value : Set.
Fixpoint eval (e: Expr): Value :=
match e with
| E a => eval a
end.
Class Quote (n: Value) : Set :=
{ quote: Expr
; eval_quote: eval quote = n }.
Program Definition quote_mult n
`{!Quote n} : Quote n :=
{| quote := E (quote (n:=n)) |}.
Set Printing Universes.
Next Obligation.
Proof.
Show Universes.
destruct Quote0 as [q eq].
Show Universes.
rewrite <- eq.
clear n eq.
Show Universes.
apply ALL.
Show Universes.
Qed.
Print quote_mult_obligation_1.
(* quote_mult_obligation_1@{} =
let Top_internal_eq_rew_dep :=
fun (A : Type@{Coq.Init.Logic.8}) (x : A) (P : forall a : A, x = a -> Type@{Top.5} (* <- XXX *))
(f : P x eq_refl) (y : A) (e : x = y) =>
match e as e0 in (_ = y0) return (P y0 e0) with
| eq_refl => f
end in
fun (n : Value) (Quote0 : Quote n) =>
match Quote0 as q return (eval quote = n) with
| {| quote := q; eval_quote := eq0 |} =>
Top_internal_eq_rew_dep Value (eval q) (fun (n0 : Value) (eq1 : eval q = n0) => eval quote = n0)
ALL n eq0
end
: forall (n : Value) (Quote0 : Quote n), eval (E quote) = n
quote_mult_obligation_1 is universe polymorphic
*)
|
