The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

In Coq 8.4 want to represent a type "Map" that is informally given by

----------------             (* zero *)
mx0 : Map

----------------             (* one *)
mx1 : Map

n : Map     m : Map    (n <> mx0 \/ n <> mx1)
--------------------------------------------------------------------
    mcons n m : Map

So I define an index set  ZZNZ  (for Zero or NonZero) and the indexed type 
Map:

Inductive ZZNZ : Set := ZZ: ZZNZ | NZ: ZZNZ.
Inductive Map: ZZNZ -> Set :=
| mx0: Map ZZ
| mx1: Map NZ
| mconsl: Map NZ -> Map ZZ -> Map NZ          (* NZ in left part *)
| mconsr: Map ZZ -> Map NZ -> Map NZ          (* NZ in right part *)
| mconsb: Map NZ -> Map NZ -> Map NZ.        (* NZ in both parts *)

Now I want to define a function "mapp: Map -> Map -> Map" given by

          mapp m n := if m = n = mx0 then mx0 else mcons m n

So I compute what the type of the result should be

Definition mappIndx (l r:ZZNZ) : ZZNZ :=
  match l, r with
    | ZZ, ZZ => ZZ
    | _, _ => NZ
end.

and want to define a function

Definition mapp (l:ZZNZ) (m:Map l) (r:ZZNZ) (n:Map zr) :
                         Map (mappIndx l r) :=
  match l, r return Map (mappIndx l r) with
    | ZZ, ZZ => mx0
    | NZ, ZZ => mconsl m n
    | ZZ, NZ => mconsr m n
    | NZ, NZ => mconsb m n
  end.

This last definition is not accepted.  How should this be defined?

A related question: is Matthieu Sozeau's "Equations" supported in Coq
8.4?  (All the files in the git repository are years old.)

Thanks for any help.

Randy