search

RyanGlScott / eliminators

Dependently typed elimination functions using singletons
BSD 3-Clause "New" or "Revised" License
27 stars 0 forks source link

Emulate Coq's induction schemes for data types that inhabit Prop #6

Open RyanGlScott opened 6 years ago

RyanGlScott commented 6 years ago

Coq generates different induction schemes depending on whether a data type inhabits Prop or not:

Inductive evenA : nat -> Type :=
  evenA0  : evenA 0
| evenASS : forall n, evenA n -> evenA (S (S n)).

Inductive evenB : nat -> Prop :=
  evenB0  : evenB 0
| evenBSS : forall n, evenB n -> evenB (S (S n)).

Check evenA_ind.
(*
evenA_ind
     : forall P : forall n : nat, evenA n -> Prop,
       P 0 evenA0 ->
       (forall (n : nat) (e : evenA n), P n e -> P (S (S n)) (evenASS n e)) ->
       forall (n : nat) (e : evenA n), P n e
*)

Check evenB_ind.
(*
evenB_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, evenB n -> P n -> P (S (S n))) ->
       forall n : nat, evenB n -> P n
*)

eliminators should permit the generation of induction schemes à la evenB_ind. (What should we call these?)