blob: 874abf49f1200c01c11e80a61255ebb415c1bc08 (
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
|
Set Implicit Arguments.
Unset Strict Implicit.
Axiom vector : Type -> nat -> Type.
Record KleeneStore i j a := kleeneStore
{ dim : nat
; peek : vector j dim -> a
; pos : vector i dim
}.
Definition KSmap i j a b (f : a -> b) (s : KleeneStore i j a) : KleeneStore i j b :=
kleeneStore (fun v => f (peek v)) (pos s).
Record KleeneCoalg (i o : Type -> Type) := kleeneCoalg
{ coalg :> forall a b, (o a) -> KleeneStore (i a) (i b) (o b) }.
Axiom free_b_dim : forall i o (k : KleeneCoalg i o) a b b' (x : o a), dim (coalg k b x) = dim (coalg k b' x).
Axiom t : Type -> Type.
Axiom traverse : KleeneCoalg (fun x => x) t.
Definition size a (x:t a) : nat := dim (traverse a a x).
Lemma iso1_iso2_2 a (y : {x : t unit & vector a (size x)}) : False.
Proof.
destruct y.
pose (X := KSmap (traverse a unit) (traverse unit a x)).
set (e :=(eq_sym (free_b_dim traverse (a:=unit) a unit x))).
clearbody e.
(** The pattern generated by change must have holes where there were implicit
arguments in the original user-provided term. This particular example fails
if this is not the case because the inferred argument does not coincide with
the one in the considered term. *)
progress (change (dim (traverse unit a x)) with (dim X) in e).
|
