Proving Transitivity of Pointwise Relations on Lists in Coq

Question

In Agda, it's quite easy to prove that if a relation R is transitive then we can define pointwise transitivity on lists:

open import Data.List

Rel : Set → Set₁
Rel A = A → A → Set

private
    variable
        A : Set
        R : A → A → Set 

data Pointwise (R : Rel A) : Rel (List A) where
    p-nil : Pointwise R [] []
    p-cons : ∀ {x y xs ys} → R x y → Pointwise R xs ys → Pointwise R (x ∷ xs) (y ∷ ys) 


Transitive : Rel A → Set
Transitive R = ∀ {x y z} → R x y → R y z → R x z  

TransitivePointwise : Transitive R → Transitive (Pointwise R)
TransitivePointwise t p-nil p-nil = p-nil
TransitivePointwise t (p-cons Rxy ps) (p-cons Ryz qs) = p-cons (t Rxy Ryz) (TransitivePointwise t ps qs) 

However, in Coq, when trying to achieve the same:

Inductive pointwise {A} (R : A -> A -> Prop) : list A -> list A -> Prop := 
| p_nil : pointwise R nil nil
| p_cons : forall {x y} {xs ys}, R x y -> pointwise R xs ys -> pointwise R (x :: xs) (y :: ys).

Theorem transitive_pointwise : forall {A} R, transitive A R -> transitive (list A) (pointwise R). 
Proof.
    unfold transitive.
    intros.
    induction H0.
    - assumption.
    -
Qed.

I get stuck because I need to recurse on H0 : pointwise R x y and H1 : pointwise R y z at the same time. I've tried using refine with a fixpoint, but in that case, Coq tells me that the fixpoint is ill-formed. It would also be nice to know why when doing destruct H0, H1, Coq gives me four cases, while Agda only gives two.

Answer 1

If you do an induction over lists (instead of over an hypothesis of type pointwise ? ?) and a few calls to inversion, it works.

Require Import Relations. 

Theorem transitive_pointwise : 
  forall {A} R, transitive A R -> transitive (list A) (pointwise R). 
Proof.
  unfold transitive; induction x. 
  - inversion 1; subst; auto. 
  - destruct y.
     +  inversion 1. 
     +  inversion 1; subst. 
        * inversion 1; subst; constructor. 
          eapply H; eauto. 
          eapply IHx; eauto. 
Qed. 

(Edited)

Ups! You can also induct over Hxy: pointwise x y :

Theorem transitive_pointwise' : 
  forall {A} R, transitive A R -> transitive (list A) (pointwise R). 
Proof.
  intros A R H x y z Hxy; revert z.
  induction Hxy. 
   - trivial. 
   - destruct z. 
    + inversion 1. 
    + inversion 1; subst; constructor. 
     * eapply H;eauto. 
     * now apply IHHxy. 
Qed.