Coq Index Relation

Question

I'm defining an indexed inductive type in Coq:

Module Typ.

  (* My index -- a t is a `t H` or a `t Z`. *)
  Inductive hz : Set := H | Z .

  (* I'd like to use this relation to constrain Cursor and Arrow. *)
  (* E.g. one specialized Cursor has type `t H -> t Z -> t Z` *)
  Inductive maxHZ : hz -> hz -> hz -> Type :=
  | HZ : maxHZ H Z Z
  | ZH : maxHZ Z H Z
  | HH : maxHZ H H H
  .

  Inductive t : hz -> Type := 
  | Num : t H
  | Hole : t H
  | Cursor : t H -> t Z
  | Arrow : forall a b c, t a -> t b -> t c
  | Sum   : forall a b c, t a -> t b -> t c
  .
End Typ.

How can I constrain my Arrow / Sum indices to be the same shape as the maxHZ relation (short of creating more constructors, like ArrowHZ : t H -> t Z -> t Z).

Depending on your final use case, you could either create a subtype of t and make Arrow satisfy the maxHZ predicate, or alternatively, you could add the relation to the constructor Arrow : forall a b c, maxHZ a b c -> t a -> t b -> t c. In all cases, you want to make maxHZ irrelevant so it doesn't bug you in proofs. Making it a boolean is likely a good idea. — ejgallego

ejgallego ejgallego · Accepted Answer · 2017-11-30T04:34:03

One approach:

(* Bring the coercion is_true into scope *)
From Coq Require Import ssreflect ssrfun ssrbool.

Module Typ.

  (* My index -- a t is a `t H` or a `t Z`. *)
  Inductive hz : Set := H | Z .

  (* I'd like to use this relation to constrain Cursor and Arrow. *)
  (* E.g. one specialized Cursor has type `t H -> t Z -> t Z` *)
  Definition maxHZ (x y z : hz) : bool :=
    match x, y, z with
    | H, Z, Z
    | Z, H, Z
    | H, H, H => true
    | _, _, _ => false
    end.

  Inductive t : hz -> Type :=
  | Num  : t H
  | Hole : t H
  | Cursor : t H -> t Z
  | Arrow : forall a b c, maxHZ a b c -> t a -> t b -> t c
  | Sum   : forall a b c, maxHZ a b c -> t a -> t b -> t c
  .
End Typ.

the other:

  Inductive t : hz -> Type :=
  | Num  : t H
  | Hole : t H
  | Cursor : t H -> t Z
  | Arrow : forall a b c, t a -> t b -> t c
  | Sum   : forall a b c, t a -> t b -> t c
  .

  Definition t_wf x (m : t x) : bool :=
    match m with
    | Arrow a b c _ _ => maxHZ a b c
    | Sum   a b c _ _ => maxHZ a b c
    | _ => true
    end.

  Definition t' x := { m : t x | t_wf x m }.
  (* This is automatically a subtype. *)

Coq Index Relation

1 Answers