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

Using Coq
1

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 (lets 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?

2

What you do almost works. You are just blocked because Hu is not impacted by your destructs 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 destructs so that Hu is also impacted by destruct).

3

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

4

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

5

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

6

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.