Is there a way to destruct and rewrite simultaneously? Here's a toy example.
Definition count_step (f : nat -> nat) (flt : forall x, f x <= x) a (rec : forall b, b < a -> nat) : nat.
refine (match f a as a0 return f a = a0 -> nat with
| 0 => fun _ => 0
| S b => fun eqa => S (rec b _)
end eq_refl
).
unfold lt; rewrite <- eqa; apply flt.
Defined.
Theorem count_step_ext x
(q : nat -> nat)
(qlt : forall x, q x <= x)
(f g : forall y, y < x -> nat)
(fgy : forall y (ylt : y < x), f y ylt = g y ylt) :
count_step q qlt x f = count_step q qlt x g.
unfold count_step.
(* destruct (q x) eqn:? written out, with rewriting (qlt x) to match *)
refine (match q x as a1 return (forall (qxa1 : q x = a1),
match a1 as a0 return (a1 = a0 -> nat) with
| 0 => fun _ : a1 = 0 => 0
| S b =>
fun eqa : a1 = S b =>
S (f b (eq_ind a1 (fun n : nat => n <= x) (eq_rect (q x) (fun n => n <= x) (qlt x) a1 qxa1) (S b) eqa))
end eq_refl =
match a1 as a0 return (a1 = a0 -> nat) with
| 0 => fun _ : a1 = 0 => 0
| S b =>
fun eqa : a1 = S b =>
S (g b (eq_ind a1 (fun n : nat => n <= x) (eq_rect (q x) (fun n => n <= x) (qlt x) a1 qxa1) (S b) eqa))
end eq_refl
) with
| 0 => _
| S b => _
end eq_refl
); intros; [ apply eq_refl | ].
rewrite fgy; apply eq_refl.
Qed.
Basically, this is easily provable by destructing q x, but attempting that
destruct (q x).
Error: Abstracting over the term "n" leads to a term
fun n0 : nat =>
match n0 as a0 return (n0 = a0 -> nat) with
| 0 => fun _ : n0 = 0 => 0
| S b =>
fun eqa : n0 = S b =>
S (f b (eq_ind n0 (fun n1 : nat => n1 <= x) (qlt x) (S b) eqa))
end eq_refl =
match n0 as a0 return (n0 = a0 -> nat) with
| 0 => fun _ : n0 = 0 => 0
| S b =>
fun eqa : n0 = S b =>
S (g b (eq_ind n0 (fun n1 : nat => n1 <= x) (qlt x) (S b) eqa))
end eq_refl which is ill-typed.
Reason is: Illegal application:
The term "eq_ind" of type
"forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y"
cannot be applied to the terms
"nat" : "Set"
"n0" : "nat"
"fun n : nat => n <= x" : "nat -> Prop"
"qlt x" : "q x <= x"
"S b" : "nat"
"eqa" : "n0 = S b"
The 4th term has type "q x <= x" which should be coercible to
"(fun n : nat => n <= x) n0".
so the problem is that we would need to simultaneously rewrite qlt x to
match the destructed q x.
Writing out the simultaneous rewrite, as above, works.
Note that it is mechanical, in that it is rewriting a nested location in which q x occurred.
But, it is quite large. Is there a shorter way to say it?
Additionally, is it possible to phrase it more succinctly without extra libraries?
I've had similar situations with needing to rewrite with a dependent rewrite too. Are those possible to handle succinctly?
Note that it is mechanical, in that it is rewriting a nested location in which q x occurred.
This is maybe not that mechanical. The problem is that not all occurrences of q x must be destructed, that's why your refine needs to introduce a qxa1 and insert it in the right places.
It's recommended to use the coq-equations library. It automates a lot of work to make dependent pattern-matching usable.
If you really want to do it by hand, one solution here is to generalize your definition, extracting the convoy pattern---without its eq_refl argument---into an auxiliary function. Notably, this avoids spelling out the return clause, because it's exactly the result type of the function, and that turns out to be precisely the help needed for destruct to work later.
Definition count_step_ (f : nat -> nat) (flt : forall x, f x <= x) a (rec : forall b, b < a -> nat)
(n : nat) : f a = n -> nat.
Proof.
refine (match n with
| 0 => fun _ => 0
| S b => fun eqa => S (rec b _)
end).
unfold lt; rewrite <- eqa; apply flt.
Defined.
Definition count_step (f : nat -> nat) (flt : forall x, f x <= x) a (rec : forall b, b < a -> nat) : nat
:= count_step_ f flt a rec (f a) eq_refl.
Equality proofs are now exposed as arguments, so your extensionality theorem must quantify over them. This strengthen the meaning of "extensionality" to also encompass proof irrelevance for this specific function. It also helps to also change the fgy assumption to say that the argument functions are proof-irrelevant. In this case it doesn't technically make a difference because y < x is already a singleton, but the change lets you avoid relying on that singleton property altogether, making the approach more generally applicable.
Theorem count_step_ext_ x
(q : nat -> nat)
(qlt : forall x, q x <= x)
(f g : forall y, y < x -> nat)
(fgy : forall y (ylt ylt' : y < x), f y ylt = g y ylt')
n m e1 e2 :
count_step_ q qlt x f n e1 = count_step_ q qlt x g m e2.
The first step of the proof is to say that n and m are equal, by n = f a _ = g a _ = m.
Proof.
assert (e3 : n = m).
{ rewrite <- e1, <- e2. reflexivity. }
Then we want to replace m with n everywhere. rewrite <- e3 won't work because the goal mentions the assumption e2 which mentions m.
This kind of dependency does not ever occur if you stick to using non-dependently typed functions. For example that's the style used throughout Software Foundations, so you get out of it with the expectation that rewrite "should just work". Dependently typed programming breaks that expectation.
The way out is to use revert on the assumption that mentions m, so m is only mentioned in the goal and the one assumption e3 that will eliminate it, by destruct (you can also use rewrite <- e3 but destruct also "garbage collects" m and e3).
revert e2. destruct e3. intros e2.
The rest of the proof is straightforward.
destruct n; cbn.
- reflexivity.
- f_equal. apply fgy.
Qed.
Finally, the extensionality theorem for the top-level wrapper is a trivial specialization of the above.
Theorem count_step_ext x
(q : nat -> nat)
(qlt : forall x, q x <= x)
(f g : forall y, y < x -> nat)
(fgy : forall y (ylt ylt' : y < x), f y ylt = g y ylt') :
count_step q qlt x f = count_step q qlt x g.
Proof.
apply count_step_ext_; auto.
Qed.