# Type (let (a, b) = ... in something a) vs. (something (let (a, b) = ... in a))

Hi,

I’m stuck on proving something that seems very basic.

``````(* The type of binary relations *)
Definition Relation (A : Type) := A -> A -> Prop.

(* A relation terminates if it has no infinite chain *)
Definition terminates (A : Type) (R : Relation A) : Prop :=
~(exists u : nat -> A, forall k, R (u k) (u (S k))).

(* The "parallel product" of two relations *)
Definition parallel_product (A B : Type) (R : Relation A) (S : Relation B) : Relation (prod A B) :=
fun ab1 ab2 =>
let (a1, b1) := ab1 in
let (a2, b2) := ab2 in
R a1 a2 /\ S b1 b2.

(* If R or S terminates, the parallel product of R and S terminates.
Let's prove this with R. *)
Lemma parallel_product_terminates_if_one_argument_terminates
(A B : Type) (R : Relation A) (S : Relation B) :
terminates A R -> terminates (prod A B) (parallel_product A B R S).
Proof.
(* Let u an infinite chain for the parallel product of R and S. *)
intros H Ha. destruct Ha as [u Hu].
(* Extract an infinite chain for R. *)
apply H. exists (fun k => let (a, b) := u k in a).
(* Let's show this is indeed an infinite chain for R. *)
intro k. unfold parallel_product in Hu.
Fail apply Hu.
(* Unable to unify "let (a1, b1) := u ?M160 in let (a2, b2) := u (Datatypes.S ?M160) in R a1 a2 /\ S b1 b2"
with "R (let (a, _) := u k in a) (let (a, _) := u (Datatypes.S k) in a)". *)
destruct (u k) as [a b] eqn:Euk. destruct (u (Datatypes.S k)) as [a' b'] eqn:EuSk.
Fail rewrite Euk in Hu.
(* Found no subterm matching "u k" in Hu. *)
``````

I can’t apply the hypothesis `Hu` as-is, apparently because it’s not under the same form (`let`s are outside the application of `R`). I tried destructing `(u k)` and `(u (Datatypes.S k))`, but Coq doesn’t accept rewriting `Hu`. Any hints on what I am doing wrong?

What you do almost works. You are just blocked because `Hu` is not impacted by your `destruct`s because it is given `forall k`.
If you instantiate `Hu` with the required value `k` (for example `specialize (Hu k).`), then you can do rewriting in `Hu` (you could also do the `specialize` before the `destruct`s so that `Hu` is also impacted by `destruct`).

Thanks, that works! Now I realize that while “simplifying” my example I did not pay enough attention — of course, `f k = g k` for some `k` in the context does not allow to deduce `forall k, f k = g k` ! What I originally tried actually was

``````set (Huk := Hu k).
``````

but then destructing `(u k)` fails:

``````Error: Abstracting over the term "p" leads to a term
fun p0 : A * B =>
let Huk0 : let (a1, b1) := p0 in let (a2, b2) := u (Datatypes.S k) in R a1 a2 /\ S b1 b2 := Hu k in
R (let (a, _) := p0 in a) (let (a, _) := u (Datatypes.S k) in a)
which is ill-typed.
Reason is: In environment
A : Type
B : Type
R : Relation A
S : Relation B
H : terminates A R
u : nat -> A * B
Hu : forall k : nat, let (a1, b1) := u k in let (a2, b2) := u (Datatypes.S k) in R a1 a2 /\ S b1 b2
k : nat
p := u k : A * B
Huk := Hu k : let (a1, b1) := p in let (a2, b2) := u (Datatypes.S k) in R a1 a2 /\ S b1 b2
p0 : A * B
The term "Hu k" has type "let (a1, b1) := u k in let (a2, b2) := u (Datatypes.S k) in R a1 a2 /\ S b1 b2"
while it is expected to have type "let (a1, b1) := p0 in let (a2, b2) := u (Datatypes.S k) in R a1 a2 /\ S b1 b2".
``````

However, it works if I instead do `specialize (Hu k)` as you recommended, and I see that it also works with

``````  assert (Huk : let (a1, b1) := u k in let (a2, b2) := u (Datatypes.S k) in R a1 a2 /\ S b1 b2) by apply Hu.
``````

I see that when I do `set (Huk := Hu k).`, `Huk` is printed in the context as

``````  Huk := Hu k : let (a1, b1) := u k in let (a2, b2) := u (Datatypes.S k) in R a1 a2 /\ S b1 b2
``````

The `name := term : type` form is something I hadn’t seen before in the context, only `name : type`. So I guess the error is somehow related to the fact that `Huk` “keeps track” of its definition as `(Hu k)`?

Indeed `Huk := Hu k : ...` adds typing constraints blocking the `destruct (u k)`.
Something close to your `set (Huk := Hu k).` but which avoids the problem is `assert (Huk := Hu k).` or `pose proof (Huk := Hu k).`.

Thanks again! I didn’t know about those useful commands `assert (name := term)` and `pose proof`.

Here’s a very short proof that uses intro patterns and the fact that `apply` can take terms, like `(contra k)` (and will see through some special cases, like when `(contra k)` has type `P /\ Q` and the goal is `P`):

``````Require Import Utf8.
Arguments terminates {A}.
Arguments parallel_product {A B}.
Lemma ppt_l {A B: Type} (R: Relation A) (Q: Relation B):
terminates R → terminates (parallel_product R Q).
Proof.
intros term_R [u contra]; apply term_R; clear term_R.
exists (λ k, fst (u k)); intro k.
now apply (contra k).
Qed.

Definition flip {A B} (x: A * B) := (snd x, fst x).

Lemma ppt_comm {A B: Type} (R: Relation A) (Q: Relation B):
terminates (parallel_product R Q) → terminates (parallel_product Q R).
Proof.
intros term_RQ [u contra]; apply term_RQ; clear term_RQ.
exists (λ k, flip (u k)); intro k; unfold flip, parallel_product in *; simpl.
now apply and_comm, (contra k).
Qed.

Lemma ppt_r {A B: Type} (R: Relation A) (Q: Relation B):
terminates Q → terminates (parallel_product R Q).
Proof. now auto using ppt_comm, ppt_l. Qed.
``````