The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

> can one do better than just to code such orders by hand? Any thoughts
appreciated...

I had a couple stabs at this to see if it could be done internally (without
opening up Coq's implementation). First off it seems that it would be quite
easy to capture this notion of (simple parametrized) inductive type:

Inductive Φ P_0 ... P_n : Type :=
| c_0 : φ_0 -> ... -> φ_m -> Φ P_0 ... P_n
| ...
| c_n : ...

where each φ would be either P_i (parametric) or Φ P_0 ... P_n (recursive).
By perhaps a list of lists of fields, and then derive the type of the
eliminator Φ_rect from that. Given that, to define a generic program would
be just applying the right arguments into the eliminators. It seems this way
cannot work out though, for two reasons:
1) one could lie perhaps, writing an eliminator that has duplicated cases
e.g. evil_bool_rect : forall P, P true -> P true -> P false -> forall b, P
b. So just the eliminator is not enough to rely on for proving generically.
2) Given one generic program (defined by generic eliminators), attempting to
write another which depends on it (e.g. Φ_compare in this case depends on
Φ_lt) seems impossible! Since it's generic we have no constructors to cause
the functions to reduce.

In that case a different approach is needed, so we take a universe of codes,
and values indexed by them (as in Peter Morris's thesis). The difficulty
coming down this road is that there is a lot of programming involved,
without dependently typed pattern matching -- I don't have a very good
solution yet (since we don't have axiom K or proof irrelevance which would
be a valuable addition..) but a variant of JMeq (for decidable indices)
seems to do the trick for this particular program (the definition of lt and
compare for the universe, I don't cover asymmetry and transitivity but they
should be analoguous).

To avoid carrying around a telescope of types (as in the Epigram versions)
I'll restrict my attention to the simpler kind of inductives (which don't
include nested/mutual induction). So there is codes for empty set, unit,
inductive, parameteric it is also closed under sums and products:

Inductive type :=
| Void | Unit | Loop | Para
| Summ : type -> type -> type
| Prod : type -> type -> type.

Values in the universe are given (parameters taken parametrically) by:

Variable Φ : type.
 
Variable params : nat.
Variable paramType : Fin params -> Type.
Variable paramLt : forall i : Fin params, paramType i -> paramType i ->
Prop.
Variable paramCompare : forall i : Fin params,
  forall x y : paramType i, Compare (paramLt i) (@eq (paramType i)) x y.
 
Inductive value : type -> Type :=
| The : value Unit
| Rec : value Φ -> value Loop
| Get : forall i : Fin params, paramType i -> value Para
| Inl : forall τ σ, value τ -> value (Summ τ σ)
| Inr : forall τ σ, value σ -> value (Summ τ σ)
| And : forall τ σ, value τ -> value σ -> value (Prod τ σ).

Then the functions (whose definitions I omit):
Definition value_lt (ρ : type) (x y : value ρ) : Prop.
Definition value_compare (ρ : type) (x y : value ρ) : Compare (value_lt ρ)
(@eq (value ρ)) x y.

allow one to give a generic definition,

Given some T : Type and Φ : type (it's encoding), as well as a function
codify : T -> value Φ params paramType Φ, and it's faithfulness proof:
codify_faithful : forall x y, codify x = codify y -> x = y.
Then compare drops out automatically.

e.g.

Definition nat_code := Summ Unit Loop.
Fixpoint nat_codify (n : nat) : value nat_code 0 no_Fin0 nat_code :=
  match n with
    | O => Inl _ _ _ _ _ (The _ _ _)
    | S n => Inr _ _ _ _ _ (Rec _ _ _ (nat_codify n))
  end.
Definition nat_compare := generic_compare
  nat nat_code 0 no_Fin0 (fun i => no_Fin0 i) (fun i => no_Fin0 i)
  nat_codify nat_codify_faithful.

Eval compute in nat_compare 3 5. (* LT *)
Eval compute in nat_compare 7 7. (* EQ *)

Using the eliminators it might be possible to derive Φ_codify automatically
but I think it's impossible to construct the proof of faithfulness for the
earlier reasons. I'm not entirely satisfied with this approach though, I
have put the whole program (there is a fair bit of machinary to get axiom
free definitions here)
 on http://github.com/odge/reg/tree , so if this is not directly useful I
hope it's at least interesting or a step in the right direction.

best wishes

-- 
View this message in context: 
http://www.nabble.com/Automatic-derivation-of-an-order-for-simple-algebraic-datatypes-in-Coq--tp21931124p22061212.html
Sent from the Coq mailing list archive at Nabble.com.