## Stream: Coq users

### Topic: Why the rewrite fails?

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

``````

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

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

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

#### 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?

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

#### 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 :)

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

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

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

#### 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?

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

#### 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?

#### Paolo Giarrusso (Oct 12 2023 at 17:33):

For instance, fixing some type errors require unfolding!

#### 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!

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

#### Karl Palmskog (Oct 13 2023 at 10:19):

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

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

``````

#### 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 `f`s, either by hand or manipulating the goal such that the rewrite tactic can do it

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

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

#### Notification Bot (Oct 13 2023 at 20:11):

Mukesh Tiwari has marked this topic as unresolved.

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

#### Paolo Giarrusso (Oct 13 2023 at 22:02):

`destruct (of_N np)` is easier, right?

#### Mukesh Tiwari (Oct 14 2023 at 08:12):

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

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

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

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

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

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

#### Quentin VERMANDE (Oct 14 2023 at 21:29):

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

#### Mukesh Tiwari (Oct 14 2023 at 21:32):

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

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

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

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

(deleted)

#### Emilio Jesús Gallego Arias (Oct 15 2023 at 01:23):

with regular Coq:

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

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

#### Paolo Giarrusso (Oct 15 2023 at 01:52):

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

#### Paolo Giarrusso (Oct 15 2023 at 01:59):

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

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

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

#### 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: Jun 13 2024 at 21:01 UTC