Require Import CpdtTactics. Inductive EN : Set := | Oe : EN | Se : ON -> EN with ON : Set := | So : EN -> ON. Fixpoint nat_of_EN (n : EN) := match n with | Oe => O | Se o => S (nat_of_ON o) end with nat_of_ON (o : ON) := match o with | So e => S (nat_of_EN e) end. Eval compute in nat_of_EN (Se (So Oe)). Fixpoint eeplus (n : EN) (m : EN) : EN := match n with | Oe => m | Se o => Se (oeplus o m) end with oeplus (o : ON) (m : EN) : ON := match o with | So e => So (eeplus e m) end. Scheme EN_induct := Induction for EN Sort Prop with ON_induct := Induction for ON Sort Prop. Lemma eeplus_n_O : forall n, eeplus n Oe = n. induction n using EN_induct with (* (P:=fun n => eeplus n Oe = n) *) (P0:=fun n => oeplus n Oe = n); crush. Qed. Hint Rewrite eeplus_n_O. Section Bez_dodatkowych_funkcji. Lemma eeplus_n_SSm : forall n m, eeplus n (Se (So m)) = Se (So (eeplus n m)). intros. induction n using EN_induct with (* (P:=fun n => eeplus n (Se (So m)) = Se (So (eeplus n m))) *) (P0:=fun n => eeplus (Se n) (Se (So m)) = Se (So (eeplus (Se n) m))); crush. Qed. Hint Rewrite eeplus_n_SSm. Lemma eeplus_commut : forall n m, eeplus n m = eeplus m n. intros. induction n using EN_induct with (* (P:=fun n => eeplus n m = eeplus m n) *) (P0:=fun n => eeplus (Se n) m = eeplus m (Se n)); crush. Qed. End Bez_dodatkowych_funkcji. Section Z_dodatkowymi_funkcjami, Fixpoint eoplus (n : EN) (m : ON) : ON := match n with | Oe => m | Se o => So (ooplus o m) end with ooplus (o : ON) (m : ON) : EN := match o with | So e => Se (eoplus e m) end. Lemma eeplus_n_Sm : forall n m, eeplus n (Se m) = Se (eoplus n m). intros. induction n using EN_induct with (* (P:=fun n => eeplus n (Se m) = Se (eoplus n m)) *) (P0:=fun n => oeplus n (Se m) = So (ooplus n m)); crush. Qed. Hint Rewrite eeplus_n_Sm. Lemma eoplus_n_Sm : forall n m, eoplus n (So m) = So (eeplus n m). intros. induction n using EN_induct with (* (P:=fun n => eoplus n (So m) = So (eeplus n m)) *) (P0:=fun n => ooplus n (So m) = Se (oeplus n m)); crush. Qed. Hint Rewrite eoplus_n_Sm. Lemma eeplus_commut' : forall n m, eeplus n m = eeplus m n. intros. induction n using EN_induct with (* (P:=fun n => eeplus n m = eeplus m n) *) (P0:=fun n => oeplus n m = eoplus m n); crush. Qed. End Z_dodatkowymi_funkcjami.