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?