## Stream: Coq users

### Topic: rewrite against dependent types

#### Andrew Miloradovsky (Nov 06 2020 at 16:49):

Hi, experienced Coq users!

I have a problem with proving a trivial-looking property which I just can't comprehend how to make Coq accept my arguments. The legend:

• We have a space of functions defined on (generally) only a subset of (in this case) natural numbers (generally a monoid).
• We want to define an equivalence relation on them where two such functions are equivalent iff one can be obtained from the other by "shifting" it, together with it's domain, by a constant argument.

Coq throws at me "ill-typed" errors no matter what I do and what tactics I try. Below is an example of a session demonstrating the problem. I'd like to understand what I'm doing wrong here, either in the proof or problem formulation itself.

``````Require Import FunctionalExtensionality.

Variable 𝔸 : Set.

Definition anchored_pattern (U: nat -> Type) := forall n, U n -> 𝔸.

Definition domain_shift (k : nat) (U : nat -> Type) : nat -> Type :=
fun i => U (i + k).

Definition pattern_shift (k : nat) U :
anchored_pattern U -> anchored_pattern (domain_shift k U) :=
fun u n => u (n + k).

Let transport {A : Type} {P : A -> Type} {x y : A}
(H : x = y) : P x -> P y :=
fun X => match H with eq_refl => X end.

Lemma domain_shift_identity :
forall U, U = domain_shift 0 U.
Proof.
intros.
unfold domain_shift.
extensionality i.
now rewrite <- plus_n_O.
Defined.

Lemma pattern_shift_identity : forall U u,
pattern_shift 0 U u = transport (domain_shift_identity U) u.
Proof.
intros.
extensionality x.
unfold pattern_shift.
extensionality p.
cbv in u.
rewrite <- (plus_n_O x) in p |- *.
(* fail *)
``````

#### Pierre-Marie Pédrot (Nov 06 2020 at 17:10):

Rewriting dependent equalities is rarely easy. HoTT had to develop a lot of machinery for it to be less painful for instance.

#### Andrew Miloradovsky (Nov 06 2020 at 17:14):

I was trying to make use of HoTT, but could only figure out how to apply the notion of transportation (eq's recursor, but with saner order of arguments, AFAIU).

#### Enrico Tassi (Nov 06 2020 at 17:58):

`destruct` is more clever in selecting the occurrences of the RHS of an equality that make the goal well typed, I don't thing rewrite does the same.

#### Andrew Miloradovsky (Nov 06 2020 at 18:11):

The state of the proof obligations looks like this by the end:

``````  U : nat -> Type
u : forall n : nat, U n -> 𝔸
x : nat
p : U (x + 0)
============================
u (x + 0) p = transport (domain_shift_identity U) u x p
``````

I'm not sure what can be destructed here besides `x`, but that wouldn't make any progress, and the proof should work with an abstract type, not just `nat`.

#### Andrew Miloradovsky (Nov 06 2020 at 18:19):

P.S. The reason I may not want to `destruct` equality hypotheses (when they're present) is because I have no control over the side which will remain after the destruction. In case of `rewrite` I know it precisely.

#### Paolo Giarrusso (Nov 06 2020 at 18:43):

You'd have to destruct a proof of x + 0 = x. Or you could swap n and k in your definitions.

(also, i and k)

(deleted)

#### Andrew Miloradovsky (Nov 06 2020 at 18:48):

``````  assert (U (x + 0) = U x) by now rewrite <- (plus_n_O x).
symmetry in H.
destruct H.
``````

got even vaguer "ill-typed" error.
Without the `symmetry` it simply does nothing.

#### Fabian Kunze (Nov 06 2020 at 18:49):

Do you know that if (e:U=U), then U=eq_refl?

#### Paolo Giarrusso (Nov 06 2020 at 18:50):

you might not even need to now that `plus_n_0` produces an `eq_refl`.

#### Andrew Miloradovsky (Nov 06 2020 at 18:51):

Perhaps (or it could be a huge term reducible to `eq_refl`). I'm actually not sure it's the only possibility anymore.

#### Paolo Giarrusso (Nov 06 2020 at 18:51):

Fabian’s proposal seems to have a type error, I think

#### Paolo Giarrusso (Nov 06 2020 at 18:52):

but Hedberg’s theorem guarantees that equalities of naturals are reflexivity

#### Paolo Giarrusso (Nov 06 2020 at 18:52):

@Andrew Miloradovsky are you sure you don’t want to swap your additions, and use the fact that `0 + x = x` holds definitionally?

#### Fabian Kunze (Nov 06 2020 at 18:52):

Well, as long as you can show UIP for U, I have the remainder here:

``````Lemma pattern_shift_identity : forall U u,
pattern_shift 0 U u = transport (domain_shift_identity U) u.
Proof.
intros.
unfold pattern_shift. unfold domain_shift_identity.
extensionality x.
set (e:=functional_extensionality _ _ _);  generalize e; clear e.
pose (f:= fun x => x + 0).
change (forall e : U = (fun i : nat => U (f i)), u (f x) = transport e u x).
replace f with (fun x : nat => x). 2:{extensionality y;unfold f. easy. }
change (fun i : nat => U i) with U. intros e.
replace e with (eq_refl U). cbn. reflexivity.
``````

#### Andrew Miloradovsky (Nov 06 2020 at 18:52):

`e = eq_refl` was meant, I suppose.

#### Fabian Kunze (Nov 06 2020 at 18:53):

Yes, e=eq_refl, sorry

#### Paolo Giarrusso (Nov 06 2020 at 18:53):

otherwise, for this proof, it’s hard without trying, but in Agda what you’d have to do is unfold things (pattern_shift, domain_shift_identity, transport) and destruct the equality

#### Paolo Giarrusso (Nov 06 2020 at 18:55):

@Fabian Kunze that equality on `U` seems false — the principle only works on naturals (or types with decidable equality), certainly not on functions

#### Fabian Kunze (Nov 06 2020 at 18:55):

Yes, in this setting, it does certainly not hold without additional axioms

#### Paolo Giarrusso (Nov 06 2020 at 18:55):

it doesn’t seem compatible with functional extensionality

#### Fabian Kunze (Nov 06 2020 at 18:58):

UIP is not compatible with FunExt? That sounds wrong.

#### Paolo Giarrusso (Nov 06 2020 at 18:59):

you’re right, they’re certainly compatible.

#### Paolo Giarrusso (Nov 06 2020 at 19:01):

Time to fetch the rooster and try out my idea.

#### Andrew Miloradovsky (Nov 06 2020 at 19:01):

@Paolo Giarrusso I changed the side on which the constant is added. But it didn't change anything, the only difference is that both of the destructions now do nothing (no errors). I've actually tried to prove it first with an abstract monoid where there are no issues w.r.t. the definition of addition, but the errors were almost exactly the same. Here I'm using `nat`s just because the code is shorter.

This also still fails:

``````  rewrite <- (plus_O_n x) in p |- *.
``````

#### Andrew Miloradovsky (Nov 06 2020 at 19:03):

Also, this is what the goal looks like after `cbv`:

``````  u x p =
match
functional_extensionality U (fun i : nat => U i) (fun i : nat => eq_refl)
in (_ = a) return (forall n : nat, a n -> 𝔸)
with
| eq_refl => u
end x p
``````

But I still have no idea how to proceed.

#### Paolo Giarrusso (Nov 06 2020 at 19:05):

Here's the result of swapping additions:

``````Variable 𝔸 : Set.

Definition anchored_pattern (U: nat -> Type) := forall n, U n -> 𝔸.

Definition domain_shift (k : nat) (U : nat -> Type) : nat -> Type :=
fun i => U (k + i).

Definition pattern_shift (k : nat) U :
anchored_pattern U -> anchored_pattern (domain_shift k U) :=
fun u n => u (k + n).

Let transport {A : Type} {P : A -> Type} {x y : A}
(H : x = y) : P x -> P y :=
fun X => match H with eq_refl => X end.

Lemma domain_shift_identity :
forall U, U = domain_shift 0 U.
Proof. reflexivity. Defined.

Lemma pattern_shift_identity : forall U u,
pattern_shift 0 U u = transport (domain_shift_identity U) u.
Proof. reflexivity. Qed.
``````

#### Paolo Giarrusso (Nov 06 2020 at 19:12):

the reason is that `x` and `0 + x` are definitionally equal (so, they're the same for typechecking), but `x + 0` is only equal propositionally, so, to use `x + 0 = x` you must use `transport`.

#### Andrew Miloradovsky (Nov 06 2020 at 19:14):

So the problem was in the use of functional extensionality:

The original proof was

``````domain_shift_identity =
fun U : nat -> Type =>
functional_extensionality U (fun i : nat => U (0 + i)) (fun i : nat => eq_refl)
: forall U : nat -> Type, U = domain_shift 0 U
``````

which should have been

``````domain_shift_identity =
fun U : nat -> Type => eq_refl
: forall U : nat -> Type, U = domain_shift 0 U
``````

Thanks a lot!

#### Paolo Giarrusso (Nov 06 2020 at 19:14):

I don't expect this fix to scale to the original problem, but unfortunately, to have any hope of using dependent types successfully, you need to understand these fine distinctions.

#### Paolo Giarrusso (Nov 06 2020 at 19:15):

sadly, for many monoids `0 + x = x` might hold only propositionally.

#### Paolo Giarrusso (Nov 06 2020 at 19:16):

worse, I don't know a way to abstract over "arbitrary monoids where `0 + x = x` holds definitionally"

#### Paolo Giarrusso (Nov 06 2020 at 19:16):

Conclusion: I would question the choice of dependent types to model partiality here:

We have a space of functions defined on (generally) only a subset of (in this case) natural numbers (generally a monoid).

#### Andrew Miloradovsky (Nov 06 2020 at 19:24):

I can try to replace it with maps from (whole) monoid to option, e.g.

``````Definition anchored_pattern : 𝕄 -> option 𝔸.
``````

It could work, but somehow this wasn't my first idea...

#### Kenji Maillard (Nov 06 2020 at 19:25):

If you have the possibility, it might even be better to fix a default value in your codomain rather than using option

#### Andrew Miloradovsky (Nov 06 2020 at 19:28):

The codomain is simply a set, usually finite or countable, in general, either option or a dedicated constant may be needed.

#### Pierre-Marie Pédrot (Nov 06 2020 at 20:12):

FTR, there is a canonical way to turn a monoid into a definitional monoid.

#### Pierre-Marie Pédrot (Nov 06 2020 at 20:13):

It relies on the availability of SProp though.

#### Pierre-Marie Pédrot (Nov 06 2020 at 20:15):

Essentially, given a monoid M : Type, dot : M -> M -> M, and one : M, you define MM := Σm : M -> M. ∃m₀ : M. ∀ x. m x = dot x m₀

#### Pierre-Marie Pédrot (Nov 06 2020 at 20:15):

a.k.a. the Yoneda embedding.

#### Pierre-Marie Pédrot (Nov 06 2020 at 20:17):

Showing the isomorphism in general requires definitional UIP which is not available by default as it breaks SN, but if your monoid has a decidable equality you can get rid of that requirement

#### Kenji Maillard (Nov 06 2020 at 20:22):

if you just ask for a retraction you don't need definitional UIP (proved here for instance)

#### Jasper Hugunin (Nov 06 2020 at 23:04):

For a HoTT-inspired solution that doesn't depend on definitional properties, you can do the following:

``````Require Import FunctionalExtensionality.

Variable A : Set.

Definition anchored_pattern (U: nat -> Type) := forall n, U n -> A.

Definition domain_shift (k : nat) (U : nat -> Type) : nat -> Type :=
fun i => U (i + k).

Definition pattern_shift (k : nat) U :
anchored_pattern U -> anchored_pattern (domain_shift k U) :=
fun u n => u (n + k).

Let transport {A : Type} {P : A -> Type} {x y : A}
(H : x = y) : P x -> P y :=
fun X => match H with eq_refl => X end.

Lemma ext_plus_n_O : (fun n => n) = (fun n => n + 0).
Proof.
extensionality n.
apply plus_n_O.
Qed.

Lemma domain_shift_identity :
forall U, U = domain_shift 0 U.
Proof.
intros U.
apply (f_equal (fun inc i => U (inc i))).
apply ext_plus_n_O.
Defined.

Lemma pattern_shift_identity : forall U u,
pattern_shift 0 U u = transport (domain_shift_identity U) u.
Proof.
intros U u.
unfold domain_shift_identity.
unfold pattern_shift.
refine (
match ext_plus_n_O as e in _ = inc'
return
(fun n => u (inc' n)) =
transport (f_equal (fun inc i => U (inc i)) e) u
with eq_refl => _ end).
simpl.
reflexivity.
Defined.
``````

The key is isolating the proof of `(fun n => n) = (fun n => n + 0)` which is shared between `domain_shift_identity` and `pattern_shift_identity`, and then a little bit of manual dependent pattern matching, since I wasn't sure how to massage the goal into a form that tactics would like.

#### Jasper Hugunin (Nov 06 2020 at 23:08):

Should work for an arbitrary monoid, even if you don't have UIP or decidable equality, or identity laws that hold up to definitional equality.

#### Andrew Miloradovsky (Nov 07 2020 at 00:33):

Thank you very much!

Indeed it does work for abstract type:

``````Require Import FunctionalExtensionality.

Variable A : Set.
Variable 𝕄 : Type.

Variable zero : 𝕄.
Variable plus : 𝕄 -> 𝕄 -> 𝕄.

Definition is_left_neutral  (e: 𝕄) := forall x: 𝕄, plus e x = x.
Definition is_right_neutral (e: 𝕄) := forall x: 𝕄, x = plus x e.
Definition is_neutral := is_left_neutral zero /\
is_right_neutral zero.
Hypothesis neutrality: is_neutral.

Definition anchored_pattern (U: 𝕄 -> Type) := forall n, U n -> A.

Definition domain_shift (k : 𝕄) (U : 𝕄 -> Type) : 𝕄 -> Type :=
fun i => U (plus i k).

Definition pattern_shift (k : 𝕄) U :
anchored_pattern U -> anchored_pattern (domain_shift k U) :=
fun u n => u (plus n k).

Let transport {A : Type} {P : A -> Type} {x y : A}
(H : x = y) : P x -> P y :=
fun X => match H with eq_refl => X end.

Lemma ext_plus_n_O : (fun n => n) = (fun n => plus n zero).
Proof.
extensionality n.
case neutrality as [ln rn].
rewrite <- rn.
reflexivity.
Qed.

Lemma domain_shift_identity :
forall U, U = domain_shift zero U.
Proof.
intros U.
apply (f_equal (fun inc i => U (inc i))).
apply ext_plus_n_O.
Defined.

Lemma pattern_shift_identity : forall U u,
pattern_shift zero U u = transport (domain_shift_identity U) u.
Proof.
intros U u.
unfold domain_shift_identity.
unfold pattern_shift.
refine (
match ext_plus_n_O as e in _ = inc'
return (fun n => u (inc' n)) =
transport (f_equal (fun inc i => U (inc i)) e) u
with eq_refl => _ end).
simpl.
reflexivity.
Defined.
``````

Next I'll try to extend this idea and use associativity to prove composition (transitivity of the relation). And if that goes well I'll finally get the equivalence classes.

#### Andrew Miloradovsky (Nov 09 2020 at 21:54):

Following Jasper's example, I was trying to prove the composition of shifts, with the same definitions and model of partiality as dependent functions, in hope that it will still pass. But nope I failed to adapt the last trick:

``````Require Import FunctionalExtensionality.

Variable 𝔸 : Set.
Variable 𝕄 : Type.

Variable plus : 𝕄 -> 𝕄 -> 𝕄.

Definition is_associative :=
forall x y z : 𝕄, (plus x (plus y z)) = (plus (plus x y) z).
Hypothesis associativity: is_associative.

Definition anchored_pattern (U: 𝕄 -> Type) := forall n, U n -> 𝔸.

Definition domain_shift (k : 𝕄) (U : 𝕄 -> Type) : 𝕄 -> Type :=
fun i => U (plus i k).

Definition pattern_shift (k : 𝕄) U :
anchored_pattern U -> anchored_pattern (domain_shift k U) :=
fun u n => u (plus n k).

Let transport {A : Type} {P : A -> Type} {x y : A}
(H : x = y) : P x -> P y :=
fun X => match H with eq_refl => X end.
Let transport' {A : Type} {P : A -> Type} {x y : A}
(H : x = y) : P y -> P x :=
match H with eq_refl => fun X => X end.

Lemma ext_plus_assoc : forall m n,
(fun l => plus (plus l m) n) = (fun l => plus l (plus m n)).
Proof.
intros.
extensionality l.
rewrite associativity.
reflexivity.
Qed.

Lemma domain_shift_composition :
forall U k l,
domain_shift k (domain_shift l U) = domain_shift (plus k l) U.
Proof.
intros.
unfold domain_shift.
apply (f_equal (fun inc i => U (inc i))).
apply ext_plus_assoc.
Defined.

Lemma pattern_shift_composition : forall U u,
forall k l : 𝕄,
pattern_shift k (domain_shift l U) (pattern_shift l U u)
= transport' (domain_shift_composition U k l)
(pattern_shift (plus k l) U u).
Proof.
intros.
unfold domain_shift_composition.
unfold pattern_shift.
refine (
match (ext_plus_assoc k l) as e in _ = inc' return
((fun n : 𝕄 => u (inc' n)) =
transport'
(f_equal (fun (inc : 𝕄 -> 𝕄) (i : 𝕄) => U (inc i)) e)
(fun n : 𝕄 => u (inc' n)))
with eq_refl => _ end).
(* fail *)
``````

I figure that I'm not allowed to use `inc'` like that, because the subexpressions are actually different. But I simply don't understand how this works in the case of identity, so can't extrapolate it properly.
How to modify it so the `associativity n k l` is taken into account?

#### Jasper Hugunin (Nov 09 2020 at 22:55):

You have the transport going the other direction, which makes things not line up in the same way. If you proceed by analogy with the identity case, it is easiest to do

``````Lemma pattern_shift_composition : forall U u,
forall k l,
pattern_shift (plus k l) U u =
transport (domain_shift_composition U k l)
(pattern_shift k (domain_shift l U) (pattern_shift l U u)).
Proof.
intros.
unfold domain_shift_composition.
unfold pattern_shift.
refine (
match (ext_plus_assoc k l) as e in _ = inc' return
((fun n => u (inc' n)) =
transport (P := anchored_pattern)
(f_equal (fun inc i => U (inc i)) e)
(fun n => u (plus (plus n k) l)))
with eq_refl => _ end).
simpl.
reflexivity.
Defined.
``````

(note that you don't need `transport'` this way)

#### Andrew Miloradovsky (Nov 10 2020 at 01:01):

Here is the relation and the properties (I messed up the order of arguments, but I'll fix that later):

``````  Definition R :
{U & anchored_pattern U} -> {V & anchored_pattern V} -> Prop.
intros XU XV.
case XU as [U u].
case XV as [V v].
exact (exists (x : 𝕄) (H : V = domain_shift x U),
pattern_shift x U u = transport H v).
Defined.

Lemma R_reflexivity : forall X : {U & anchored_pattern U},
R X X.
Proof.
intros.
unfold R.
case X as [U u].
exists zero.
exists (domain_shift_identity U).
apply pattern_shift_identity.
Qed.

Lemma R_transitivity : forall (XU : {U & anchored_pattern U})
(XV : {V & anchored_pattern V})
(XW : {W & anchored_pattern W}),
R XV XU -> R XW XV -> R XW XU.
Proof.
intros ??? HUV HVW.
unfold R in *.
case XU as [U u].
case XV as [V v].
case XW as [W w].
destruct HUV as [x Hx].
destruct HVW as [y Hy].
exists (plus x y).
destruct Hx as [Hx Kx].
destruct Hy as [Hy Ky].
subst U V.
simpl in Kx, Ky.
subst u v.
exists (domain_shift_composition W x y).
simpl.
f_equal.
rewrite (pattern_shift_composition W w x y).
reflexivity.
Qed.
``````

Huge thanks!

Last updated: Sep 26 2023 at 12:02 UTC