Stream: Coq users

Topic: Why the rewrite fails?


view this post on Zulip Mukesh Tiwari (Oct 10 2023 at 19:03):

Hi everyone,

I have a term Hb: fn = eq_rect (S n0) (λ t0 : nat, Fin.t t0) (FS t) (S n) Ha in the context and I want to replace eq_rect (S n0) (λ t0 : nat, Fin.t t0) (FS t) (S n) Ha by (FS t) using rew_const, but it is not working.

 Require Import List Utf8 Vector Fin Psatz.
 Import Notations.

 Definition fin (n : nat) : Type := {i | i < n}.


  Theorem Fin_to_fin :  (n : nat), Fin.t n -> fin n.
  Proof.
    induction n;
    intro fn.
    + refine match fn with end.
    +
      refine
        (match fn as fn' in Fin.t n'
          return  (pf : n' = S n),
          fn = @eq_rect _ n' (fun t => Fin.t t) fn' _ pf -> _
        with
        | Fin.F1 => fun Ha Hb => (exist _ 0 _)
        | Fin.FS t => fun  Ha Hb => _
        end eq_refl eq_refl).
      ++ abstract nia.
      ++
          Check rew_const.
          (*
           ∀ (A P : Type) (x y : A) (e : x = y) (k : P),
            eq_rect x (λ _ : A, P) k y e = k
          *)
          (* why is this rewrite not working? Technically,
            I don't need to know fn = FS t but I am
            curious about why rewrite fails *)
          Fail rewrite rew_const in Hb.

  Admitted.

view this post on Zulip Quentin VERMANDE (Oct 10 2023 at 19:20):

Hi, in order to rewrite rew_const, the (fun t => Fin.t t) term would have to be a constant function. In this case, since you manipulate the equality on nat, which is decidable, you can use Eqdep_dec.eq_rect_eq_dec instead.

view this post on Zulip Mukesh Tiwari (Oct 10 2023 at 19:29):

@Quentin VERMANDE

Thanks! I see my mistake. Btw, rewrite <- Eqdep_dec.eq_rect_eq_dec in Hb. is also not working because eq_rect p Q x p h is different from the one I have eq_rect (S n0) (λ t0 : nat, Fin.t t0) (FS t) (S n) Ha .

Eqdep_dec.eq_rect_eq_dec
     :  A : Type,
         (∀ x y : A, {x = y} + {x  y})
           (p : A) (Q : A  Type) (x : Q p) (h : p = p),
             x = eq_rect p Q x p h

I need more general lemma, something like this:

  A : Type,
   (∀ x y : A, {x = y} + {x  y})
      (p  q : A) (Q : A  Type) (x : Q p) (h : p = q),
      x = eq_rect p Q x q h

view this post on Zulip Quentin VERMANDE (Oct 10 2023 at 19:39):

Oops, indeed, you first need to change (S n0) or (S n) into the other one. This is always painful because there usually are e.g. hypotheses which make the goal ill-typed. In this case, asserting the equality (S n0 = S n), reverting fn and Ha back to the goal and rewriting (backwards) the asserted equality works.

view this post on Zulip Mukesh Tiwari (Oct 10 2023 at 19:42):

Surprisingly, I can't find the lemma of more general type (but it could be also I am tired and I need to go to sleep rather than theorem proving :) . @Quentin VERMANDE Can you post the code?

view this post on Zulip Quentin VERMANDE (Oct 10 2023 at 19:46):

I do not think it exists, since it is strictly more general than the one in the library. I did

assert (S n0 = S n) by exact Ha.
revert Ha fn Hb.
rewrite <- H.
intros Ha fn.
rewrite <- Eqdep_dec.eq_rect_eq_dec.
intro Hb.

It is probably far from optimal though, I have not written vanilla coq for some time.

view this post on Zulip Mukesh Tiwari (Oct 10 2023 at 19:52):

Nice! You managed to avoid the Abstracting over ... error so it is far better than optimal code :)

view this post on Zulip Quentin VERMANDE (Oct 10 2023 at 20:04):

Yes, this is a very frequent error when rewriting in presence of dependent types. Basically, every time you have to make sure that when you rewrite a term, there is nothing that uses the term (hypothesis or part of the goal) that would make the goal ill-typed after the rewrite. In you case, "rewrite H" would fail because of the (FS t) term in the goal which uses n0.

view this post on Zulip Quentin VERMANDE (Oct 10 2023 at 20:05):

Actually, you can even assert n0 = n and use subst n0, which is maybe brutal but quite safer, since you are sure that every occurence of n0 disappears.

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 20:09):

you can do something like

      injection Ha;intros Ha'.
      assert (Ha'' : f_equal S Ha' = Ha) by apply Peano_dec.UIP_nat.
      destruct Ha'',Ha'.
      simpl in Hb.
      (* Hb : fn = FS t *)

destruct on an equality where the right hand side is a variable which doesn't appear on the left hand side always works

view this post on Zulip Mukesh Tiwari (Oct 12 2023 at 16:07):

@Quentin VERMANDE I am thinking about what you have written and I am trying to figure out a general recipe for avoiding Abstracting over ... in Coq which I often struggles. The basic idea, as I understand from your answer, is: if I want to replace a term a by another term b (a = b), I should make sure that a is not used in either in the context or in the goal. If so, I need to generalise the theorem (the way you did by creating a duplicate proof and reverting all the relevant information back to goal) and then use rewrite. Did I get this right? Do you have any other suggestion to deal with Abstracting over ... error?

view this post on Zulip Quentin VERMANDE (Oct 12 2023 at 16:55):

I used to struggle a lot with that, too. Duplicating the equality is quite specific to your example, simply reverting things is usually enough. Also, your protocol would work, but if I can be very nitpicky, it is a little too restrictive the way I read it. You actually only need to revert the terms whose type would break the typing of the goal after the rewrite. For instance, if in your example you were to rewrite n into n0, you would not need to revert IHn, whereas if you were to rewrite Ha directly, you would get an error because FS t has type Fin.t (S n0), whereas after the rewrite it would be expected to have type Fin.t (S n) (which is what the error message tells you, however hard it is to read). Also, it did not happen here, but it may happen that you have to rewrite specific occurences of your term (although I can not find an example off the top of my head). As for suggestions, I found subst to be the safest solution, or destruct as Gaëtan Gilbert mentioned, but that only works when you rewrite a variable into something, and you may have reasons to want to keep the variable or not to rewrite everywhere.

view this post on Zulip Paolo Giarrusso (Oct 12 2023 at 17:32):

I wonder (1) if the general advice should be to actually look at the generated code and type error together, then figure out the type error, and (2) if there are ways to help that process — to get Coq to print the generated term better, or whether Equations has tool that help?

view this post on Zulip Paolo Giarrusso (Oct 12 2023 at 17:33):

For instance, fixing some type errors require unfolding!

view this post on Zulip Paolo Giarrusso (Oct 12 2023 at 17:38):

If A : forall x, P x -> Q x, B := A e, and your goal mentions B arg, you'll probably need to unfold B before you can replace e by e', because B's type is too specific. But if we only had the specialized version of B, this approach won't work; we might need to generalize over B, or to go patch B to make it more flexible!

view this post on Zulip Mukesh Tiwari (Oct 13 2023 at 09:53):

It would be great if we could collect some examples, very similar to lisp-koans [1], to make dependent type rewriting accessible to mass audience.

[1] https://github.com/google/lisp-koans

view this post on Zulip Karl Palmskog (Oct 13 2023 at 10:19):

one possible place for such examples? https://github.com/tchajed/coq-tricks/

view this post on Zulip Mukesh Tiwari (Oct 13 2023 at 10:44):

Why does the second last and last [1] rewrite fails? In this rewrite, I am trying to replace S n0 by S n to emphasise if I get the idea of generalisation but it seems not. I have generalised the goal but the rewrite still fails.

Require Import List Utf8 Vector Fin Psatz.
Import Notations.

Section Iso.


  Definition fin (n : nat) : Type := {i | i < n}.


  Theorem Fin_to_fin :  (n : nat), Fin.t n -> fin n.
  Proof.
    induction n;
    intro fn.
    + refine match fn with end.
    +
      refine
        (match fn as fn' in Fin.t n'
          return  (pf : n' = S n),
          fn = @eq_rect _ n' (fun t => Fin.t t) fn' _ pf -> _
        with
        | Fin.F1 => fun Ha Hb => (exist _ 0 _)
        | Fin.FS fw => fun  Ha Hb => _
        end eq_refl eq_refl).
      ++ abstract nia.
      ++
        (* In this rewrite, I am trying to
          replace (S n0) by (S n) because
          (FS t) has type (Fin.t (S n0)) and
          it's changing the type to (Fin.t (S n))
          so fail is fine and I, hopefully, understand this.
        *)

        Fail rewrite Ha in Hb.

        (* Lets revert Hb and fw whose
          types involve n0
        *)
        revert fw Hb.

         (* WHY DOES THIS REWRITE FAILS?
          Now our goal is general enough
          where we can replace n0 by n.
          I DON'T UNDERSTAND THIS.
        *)
        Fail rewrite Ha.

        (* even if I generalised Ha *)
        assert (Hb : S n0 = S n) by apply Ha.
        revert Ha.

       (* I DON'T UNDERSTAND THIS *)
        Fail rewrite Hb.


  Admitted.

[1] https://gist.github.com/mukeshtiwari/ab87223430786a46aa62161cc3a70763#file-dep_rewrite-v-L63

view this post on Zulip Gaëtan Gilbert (Oct 13 2023 at 11:13):

rewrite is always "along" a predicate: you need a function f : forall x, x = right_hand_side -> Type such that f left_hand_side the_eq_proof is convertible to the goal
(when the equality proof doesn't appear in the goal you can simplify to finding f : forall x, Type such that f left_hand_side is convertible to the goal)
so here f (S n0) Ha would have to be convertible to your goal ∀ fw : t n0, fn = eq_rect (S n0) (λ t0 : nat, t t0) (FS fw) (S n) Ha → {i : nat | i < S n0}
the error says

Abstracting over the terms "S n0" and "Ha" leads to a term
λ (y : nat) (Ha0 : y = S n),
   fw : t n0, fn = eq_rect y  t0 : nat, t t0) (FS fw) (S n) Ha0  {i : nat | i < y}
which is ill-typed.

ie the f it generated is ill typed

dependent rewrite is all about figuring out how to generate such fs, either by hand or manipulating the goal such that the rewrite tactic can do it

view this post on Zulip Quentin VERMANDE (Oct 13 2023 at 11:38):

Specifically for this example, the first two tries is bound to fail since Ha appears in the goal, so you have to revert it (that which you guessed). In the last try, you are rewriting S n0 into S n, so the type of fw, which is t n0, does not get rewritten into t n, hence the failure. You would need to assert n0 = n.

view this post on Zulip Mukesh Tiwari (Oct 13 2023 at 11:54):

Wow! I can't believe I made such a silly mistake :) Now rewrite works the way I want. Thanks @Quentin VERMANDE @Gaëtan Gilbert and @Paolo Giarrusso for the help. It is one step closer to understanding dependent type rewriting.

Best,
Mukesh

  Theorem Fin_to_fin :  (n : nat), Fin.t n -> fin n.
  Proof.
    induction n;
    intro fn.
    + refine match fn with end.
    +
      refine
        (match fn as fn' in Fin.t n'
          return  (pf : n' = S n),
          fn = @eq_rect _ n' (fun t => Fin.t t) fn' _ pf -> _
        with
        | Fin.F1 => fun Ha Hb => (exist _ 0 _)
        | Fin.FS fw => fun  Ha Hb => _
        end eq_refl eq_refl).
      ++ abstract nia.
      ++
        (* In this rewrite, I am trying to
          replace (S n0) by (S n) because
          (FS t) has type (Fin.t (S n0)) and
          it's changing the type to (Fin.t (S n))
          so fail is fine.
        *)
        Fail rewrite Ha in Hb.
        (* Lets revert Hb and fw whose
          types involve n0
        *)
        revert fw Hb.
         (* WHY DOES THIS REWRITE FAILS?
          Now our goal is general enough
          where we can replace n0 by n.
        *)
        Fail rewrite Ha.
        (* even if I generalised Ha *)
        assert (Hb : n0 = n) by nia.
        revert Ha.
       (*  Yay! Finally, it works *)
        rewrite Hb; clear Hb.

view this post on Zulip Notification Bot (Oct 13 2023 at 20:11):

Mukesh Tiwari has marked this topic as unresolved.

view this post on Zulip Mukesh Tiwari (Oct 13 2023 at 20:14):

How can I rewrite Ha in the goal? I have hard time generalising it.

Require Import Lia
  Coq.Unicode.Utf8
  Coq.Bool.Bool
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith
  Coq.Lists.List.


  Definition np_total (np : N) :  (np <? 256 = true)%N ->  byte.
  Proof.
    intros H.
    pose proof of_N_None_iff np as Hn.
    destruct (of_N np) as [b | ].
    + exact b.
    + exfalso; abstract (apply N.ltb_lt in H; intuition nia).
  Defined.


  Lemma np_true : forall (np : N) (H : (np <? 256)%N = true) x,
    of_N np = Some x -> np_total np H = x.
  Proof.
    unfold np_total; intros * Ha.
    (* I want to rewrite Ha in the goal *)
    Fail rewrite Ha.
    assert (Hb : of_N np = Some x) by apply Ha.
    revert Ha H.
    Fail rewrite Hb.
    (* I need to generalise np somehow but I don't know how *)

view this post on Zulip Paolo Giarrusso (Oct 13 2023 at 22:02):

destruct (of_N np) is easier, right?

view this post on Zulip Mukesh Tiwari (Oct 14 2023 at 08:12):

destruct (of_N np) is not working. I am getting the Abstracting over the term .. error.

view this post on Zulip Mukesh Tiwari (Oct 14 2023 at 08:22):

Just for the record, I have a working solution but I am looking for some more ideas. This time I am determined to conquer abstracting over .... error :)

Lemma np_true : forall (np : N) (H : (np <? 256)%N = true) x,
    of_N np = Some x -> np_total np H = x.
  Proof.
    unfold np_total; intros * Ha.
    (* I want to rewrite Ha in the goal *)
    Fail rewrite Ha.
    assert (Hb : of_N np = Some x) by apply Ha.
    revert Ha H.
    Fail rewrite Hb.
    (* This works! *)
    generalize (of_N_None_iff np).
    rewrite Hb.

view this post on Zulip Quentin VERMANDE (Oct 14 2023 at 08:27):

Just in case an explanation of what happens is useful, Ha does not appear in the goal, so the issue is not there. Somewhere in the error message, you should see cannot be applied to the term <term> : <type> which tells you which term breaks the typing. In this case, it is of\_N\_None\_iff np in which type the thing you want to rewrite appears. After the rewrite, it would need to have type Some x = None <-> (255 < np)%N, so you have to generalize it in order to also rewrite its type.

view this post on Zulip Mukesh Tiwari (Oct 14 2023 at 20:25):

@Quentin VERMANDE I have a slightly old definition which is more complicated (for no reason) which I wrote before the simple one and now I am trying to prove the same theorem again for this definition. I understand why first rewrite fails because Ha appears in the goal. I generalise it but I can't figure out why second rewrite fails. Any idea why?

Require Import List Utf8 Vector Fin Psatz.
Import Notations ListNotations.


Require Import Lia
  Coq.Unicode.Utf8
  Coq.Bool.Bool
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith
  Coq.Lists.List.

Open Scope N_scope.

(* a more complicated definition, for no reason, that I wrote before the simple one *)
Definition np_total (np : N):  (np <? 256 = true) ->  byte.
Proof.
  intros H.
  refine(match (np <? 256) as b return  mp, np = mp ->
      (mp <? 256) = b -> _ with
   | true => fun mp Hmp Hmpt =>
      match of_N mp as npt return _ = npt -> _ with
      | Some x => fun _ => x
      | None => fun Hf => _
      end eq_refl
   | false => fun mp Hmp Hmf => _
  end np eq_refl eq_refl).
  abstract(
  apply of_N_None_iff in Hf;
  apply N.ltb_lt in Hmpt; nia).
  abstract (subst; congruence).
Defined.

(* Now I am trying to prove the same theorem again *)
Lemma np_true : forall np (Ha : np <? 256 = true) x,
  of_N np = Some x -> np_total np Ha = x.
Proof.
  intros * Hb; unfold np_total.
  Fail rewrite Ha.
  (* Goal: I want to rewrite Ha but it appears in
    in the term np_total_tmp_subproof0 np Ha mp Hmp Hmf
    so generalize it
  *)
  generalize (np_total_subproof0 np Ha) as f.
  (* I can't understand this error! *)
  rewrite Ha.

view this post on Zulip Quentin VERMANDE (Oct 14 2023 at 20:45):

Oof, got it. This one is horrible, I had to Set Printing All to inspect the term and guess the occurrences to rewrite. The last eq\_refl’ has type np <? 256 = np <? 256 but after the rewrite it needs to have type np <? 256 = true, so you need to generalize this term and rewrite every occurences 2 and 3 of np <? 256`.

view this post on Zulip Mukesh Tiwari (Oct 14 2023 at 20:51):

For me Set Printing All does not change anything. I don't see any difference in two outputs [1].

[1] https://gist.github.com/mukeshtiwari/15d25c5b66074b260421ae98400c2632

view this post on Zulip Quentin VERMANDE (Oct 14 2023 at 21:29):

You should see the implicit argument of eq_refl in the goal.

view this post on Zulip Mukesh Tiwari (Oct 14 2023 at 21:32):

Could you post a screen shot of both? Possibly I am missing something obvious.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 01:12):

Indeed you need to be careful when generalizing, using ssreflect:

  Lemma np_true : forall (np : N) (H : (np <? 256)%N = true) x,
    of_N np = Some x -> np_total np H = x.
  Proof.
    unfold np_total => np h_range b.
    move: (of_N np) (of_N_None_iff np).
    by case => // b' _ [].
  Qed.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 01:13):

The proof itself is quite straightforward, but requires discipline due to the definition doing matches on proofs.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 01:14):

In this case, you need to convert to indexes all the non-uniform parameters, _à la_ convoy. This is often just routine.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 01:16):

(deleted)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 01:23):

with regular Coq:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 01:23):

Lemma np_true : forall (np : N) (H : (np <? 256)%N = true) x,
    of_N np = Some x -> np_total np H = x.
  Proof.
    unfold np_total; intros np h_range b.
    generalize (of_N np) (of_N_None_iff np).
    now intros o; destruct o; congruence.
  Qed.

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 01:50):

@Mukesh Tiwari with VsCoq1/coqide you can't use Set Printing ... literally, you need the matching IDE command

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 01:52):

"Coq: Display All Basic Low-level Contents."

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 01:59):

https://github.com/coq-community/vscoq/issues/81

view this post on Zulip Mukesh Tiwari (Oct 15 2023 at 09:46):

It seems I am almost there. How can I turn an expression forall (e : (np <? 256) = (np <? 256)) into forall (u : bool), u = (np <? 256), (e : (np <? 256) = u) ? @Quentin VERMANDE Now I see what you meant.

Lemma np_true : forall np (Ha : np <? 256 = true) x,
  of_N np = Some x -> np_total np Ha = x.
Proof.
  intros * Hb; unfold np_total.
  (* Goal: I want to rewrite Ha but it appears in
    in the term np_total_tmp_subproof0 np Ha mp Hmp Hmf
    so generalize it
   *)
  Set Printing All.
  generalize (np_total_subproof0 np Ha) as f.
  generalize (eq_refl (np <? 256)).
  Unset Printing All.
  (* How can I turn
   forall (e :  (np <? 256) = (np <? 256))
    into
    forall (u : bool), u = (np <? 256), (e : (np <? 256) = u)  -> ....
  *)

view this post on Zulip Paolo Giarrusso (Oct 16 2023 at 07:13):

With the simplified definition you can also skip Hb:

Lemma np_true : forall (np : N) (H : (np <? 256)%N = true) x,
  of_N np = Some x -> np_total np H = x.
Proof.
  unfold np_total; intros * Ha.
  generalize (of_N_None_iff np).
  Succeed solve [destruct (of_N np); congruence].
  rewrite Ha. reflexivity.
Qed.

view this post on Zulip Paolo Giarrusso (Oct 16 2023 at 07:26):

here's a version for the more complex one:

Lemma np_true : forall np (Ha : np <? 256 = true) x,
  of_N np = Some x -> np_total np Ha = x.
Proof.
  intros * Hb; unfold np_total.
  generalize (np_total_subproof0 np Ha) as f.
  generalize (eq_refl (np <? 256)) as Hlts.
  generalize (np <? 256) at 2 3.
  intros b **.
  destruct b; [| congruence].
  generalize  Hf, np_total_subproof np np eq_refl Hlts Hf).
  rewrite Hb.
  reflexivity.
Qed.

Last updated: Oct 13 2024 at 01:02 UTC