Skip to content

Instantly share code, notes, and snippets.

@co-dan co-dan/induction.v
Created Jan 16, 2015

Embed
What would you like to do?
Inductive gorgeous : nat -> Prop :=
g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).
Fixpoint gorgeous_ind_max (P: forall n, gorgeous n -> Prop) (f : P 0 g_0)
(f0 : forall (m : nat) (e : gorgeous m),
P m e -> P (3+m) (g_plus3 m e))
(f1 : forall (m : nat) (e : gorgeous m),
P m e -> P (5+m) (g_plus5 m e))
(n : nat) (e: gorgeous n) : P n e :=
match e in (gorgeous n0) return (P n0 e) with
| g_0 => f
| g_plus3 n0 g0 => f0 n0 g0 (gorgeous_ind_max P f f0 f1 n0 g0)
| g_plus5 n0 g0 => f1 n0 g0 (gorgeous_ind_max P f f0 f1 n0 g0)
end.
Check gorgeous_ind_max.
(*
gorgeous_ind_max
: forall P : forall n : nat, gorgeous n -> Prop,
P 0 g_0 ->
(forall (m : nat) (e : gorgeous m), P m e -> P (3 + m) (g_plus3 m e)) ->
(forall (m : nat) (e : gorgeous m), P m e -> P (5 + m) (g_plus5 m e)) ->
forall (n : nat) (e : gorgeous n), P n e
*)
Check gorgeous_ind.
(*
gorgeous_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, gorgeous n -> P n -> P (3 + n)) ->
(forall n : nat, gorgeous n -> P n -> P (5 + n)) ->
forall n : nat, gorgeous n -> P n
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.