Quelle  change_pattern.v   Sprache: Coq

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).
Abort.