The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

On 28/07/2020 15:32, Adam Chlipala wrote:
> That's harder to do with the solution where you build a list and call a
> Gallina function, but it only requires standard use of heterogeneous
> list types (e.g., see Chapter 9 of CPDT
> <http://adam.chlipala.net/cpdt/>).  Type inference is quite smart enough
> to reconstruct a list of types from a (heterogeneous) list of values of
> those types.  And, if working with heterogeneous lists doesn't seem
> worth the trouble, you can use a notation that constructs a tuple and
> passes it off to Ltac, which can do recursive traversal of tuples as
> easily as of various list types.

Using pairs + ltac for this is a good idea! I implemented it below.

I also solved the 'problem' that list notation had to be used inside
`chain ... endchain`. Now we can write `chain 1 <=, 2 <=, 3` (note the
comma). This solution uses a scope in which `<=,` is an infix for pairs.

> red {X Y : Type} : phi X -> phi Y -> Prop  where phi : Type -> Type

In the code below, I used a slightly different type of `red`, but you
should be able to adapt the code to your type.


```
(* This is a bit different than asked *)
Axiom phi : Type -> Type.
Axiom red : forall {X : Type}, X -> phi X -> Prop.

Ltac chainToProp' xs :=
  lazymatch xs with
  | pair ?x (pair ?y ?xs) =>
    let z := chainToProp' (pair y xs) in
    constr:(red x y /\ z)
  | pair ?x ?y => constr:(red x y)
  end.

Ltac chainToProp xs :=
  let z := chainToProp' xs in
  exact z.

Axiom X0 : Type.
Axiom a : X0.
Axiom b : phi X0.
Axiom c : phi (phi X0).
Axiom d : phi (phi (phi X0)).

Declare Scope chain.
Delimit Scope chain with chain_scope.
Notation "x <=, y" := (pair x y) (at level 80, right associativity, only
parsing) : chain.
Notation "'chain' xs 'endchain'" := (ltac:(chainToProp (xs %
chain_scope))) (only parsing).
Check chain a <=, b <=, c <=, d endchain.
(* red a b /\ red b c /\ red c d *)
(*      : Prop *)
```