Stream: Coq users

Topic: rewrite against dependent types


view this post on Zulip 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:

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 18:43):

(also, i and k)

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 18:44):

(deleted)

view this post on Zulip Andrew Miloradovsky (Nov 06 2020 at 18:48):

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.

view this post on Zulip Fabian Kunze (Nov 06 2020 at 18:49):

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

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 18:50):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 18:51):

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

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 18:52):

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

view this post on Zulip 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?

view this post on Zulip 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.
  (*e = eq_refl*) admit.
Admitted.

view this post on Zulip Andrew Miloradovsky (Nov 06 2020 at 18:52):

e = eq_refl was meant, I suppose.

view this post on Zulip Fabian Kunze (Nov 06 2020 at 18:53):

Yes, e=eq_refl, sorry

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Fabian Kunze (Nov 06 2020 at 18:55):

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

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 18:55):

it doesnโ€™t seem compatible with functional extensionality

view this post on Zulip Fabian Kunze (Nov 06 2020 at 18:58):

UIP is not compatible with FunExt? That sounds wrong.

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 18:59):

youโ€™re right, theyโ€™re certainly compatible.

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 19:01):

Time to fetch the rooster and try out my idea.

view this post on Zulip 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 nats just because the code is shorter.

This also still fails:

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 19:15):

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

view this post on Zulip 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"

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pรฉdrot (Nov 06 2020 at 20:12):

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

view this post on Zulip Pierre-Marie Pรฉdrot (Nov 06 2020 at 20:13):

It relies on the availability of SProp though.

view this post on Zulip 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โ‚€

view this post on Zulip Pierre-Marie Pรฉdrot (Nov 06 2020 at 20:15):

a.k.a. the Yoneda embedding.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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: Jan 31 2023 at 13:02 UTC