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.
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.
@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
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.
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?
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.
Nice! You managed to avoid the Abstracting over ...
error so it is far better than optimal code :)
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.
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.
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
@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?
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.
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?
For instance, fixing some type errors require unfolding!
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!
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
one possible place for such examples? https://github.com/tchajed/coq-tricks/
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
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
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
.
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.
Mukesh Tiwari has marked this topic as unresolved.
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 *)
destruct (of_N np)
is easier, right?
destruct (of_N np)
is not working. I am getting the Abstracting over the term ..
error.
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.
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.
@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.
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`.
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
You should see the implicit argument of eq_refl
in the goal.
Could you post a screen shot of both? Possibly I am missing something obvious.
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.
The proof itself is quite straightforward, but requires discipline due to the definition doing matches on proofs.
In this case, you need to convert to indexes all the non-uniform parameters, _à la_ convoy. This is often just routine.
(deleted)
with regular Coq:
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.
@Mukesh Tiwari with VsCoq1/coqide you can't use Set Printing ...
literally, you need the matching IDE command
"Coq: Display All Basic Low-level Contents."
https://github.com/coq-community/vscoq/issues/81
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) -> ....
*)
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.
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