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 *)
```

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

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

`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.

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`

.

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.

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)

Added

```
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.

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

you might not even need to now that `plus_n_0`

produces an `eq_refl`

.

Perhaps (or it could be a huge term reducible to `eq_refl`

). I'm actually not sure it's the only possibility anymore.

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

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

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

holds definitionally?

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.
(*e = eq_refl*) admit.
Admitted.
```

`e = eq_refl`

was meant, I suppose.

Yes, e=eq_refl, sorry

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

@Fabian Kunze that equality on `U`

seems false โ the principle only works on naturals (or types with decidable equality), certainly not on functions

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

it doesnโt seem compatible with functional extensionality

UIP is not compatible with FunExt? That sounds wrong.

youโre right, theyโre certainly compatible.

Time to fetch the rooster and try out my idea.

@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 |- *.
```

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.

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.
```

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`

.

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!

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.

sadly, for many monoids `0 + x = x`

might hold only propositionally.

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

holds definitionally"

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

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

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

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

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

It relies on the availability of SProp though.

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โ

a.k.a. the Yoneda embedding.

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

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

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.

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.

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.

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?

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)

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: Jan 31 2023 at 13:02 UTC