Inductive nat : type := | O : nat | S : V (x: nat). nat. Recursive plus (a: nat) (b: nat) [0] : nat := match a with ( b, \ (a1: nat). S (plus a1 b) ). Inductive eq (A: type) (a: A) : V (b: A). type := | eqrefl: eq A a a. Lemma eqind : V (A:type). (V (a:A). (V (P:V (x:A). (type)). (V (Pa:P a). (V (b:A). (V (eqab:eq A a b). (P b)))))). exact ( \ (A: type). \ (a: A). \ (P: V (x: A). type). \ (Pa: P a). \ (b: A). \ (eqab: eq A a b) . match eqab return (P b) with ( \ (A: type). \ (a: A). Pa ) ). Qed. Lemma eqSnat: V (a: nat). V (b: nat). V (eqab: eq nat a b). eq nat (S a) (S b). intro. intro. intro. factorize b. apply eqind. exact nat. exact a. simpl. apply eqrefl. apply eqab. Qed. Lemma eqcomm: V (A: type). V (a: A). V (b: A). V (eqab: eq A a b). eq A b a. intro. intro. intro. intro. factorize b. apply eqind. apply A. apply a. simpl. apply eqrefl. apply eqab. Qed. Inductive list (A: type) : type := | nil: list A | conc: V (a: A). V (l: list A). list A. Recursive length (A: type) (l: list A) [1] : nat := match l return nat with ( \ (A: type). O, \ (A: type). \ (a: A). \ (l2: list A). S (length A l2) ). Recursive app (A: type) (l1: list A) (l2: list A) [1] : list A := match l1 return (list A) with ( \ (A: type). l2, \ (A: type). \ (a: A). \ (l12: list A). conc A a (app A l12 l2) ). Lemma applength: V (A: type). V (l1: list A). V (l2: list A). eq nat (length A (app A l1 l2)) (plus (length A l1) (length A l2)). intro. intro. factorize l1. apply listinduc. exact A. simpl. intro. apply eqrefl. intro. intro. intro. simpl. intro. simpl in Predindind11. intro. apply eqSnat. apply Predindind11. Qed. Lemma appnil: V (A: type). V (l: list A). eq (list A) (app A l (nil A)) l. intro. intro. factorize l. apply listinduc. exact A. simpl. apply eqrefl. simpl. intro. intro. intro. factorize (app A l0 (nil A)). apply eqind. apply (list A). apply l0. simpl. apply eqrefl. apply eqcomm. apply Predindind11. Qed. Lemma appassoc: V (A: type). V (l1: list A). V (l2: list A). V (l3: list A). eq (list A) (app A (app A l1 l2) l3) (app A l1 (app A l2 l3)). intro. intro. factorize l1. apply listinduc. exact A. simpl. intro. intro. apply eqrefl. simpl. intro. intro. intro. intro. intro. factorize (app A l (app A l2 l3)). apply eqind. exact (list A). exact (app A (app A l l2) l3). simpl. apply eqrefl. apply Predindind11. Qed. Recursive rev (A: type) (l: list A) [1] : list A := match l with ( \ (A: type). nil A, \ (A: type). \ (a: A). \ (l: list A). app A (rev A l) (conc A a (nil A)) ). Lemma apprev: V (A: type). V (l1: list A). V (l2: list A). eq (list A) (rev A (app A l1 l2)) (app A (rev A l2) (rev A l1)). intro. intro. factorize l1. apply listinduc. exact A. simpl. intro. apply eqcomm. exact (appnil A (rev A l2)). simpl. intro. intro. intro. intro. factorize (rev A (app A l l2)). apply eqind. exact (list A). exact (app A (rev A l2) (rev A l)). simpl. factorize (app A (app A (rev A l2) (rev A l)) (conc A a (nil A))). apply eqind. exact (list A). exact (app A (rev A l2) (app A (rev A l) (conc A a (nil A)))). simpl. apply eqrefl. apply eqcomm. apply appassoc. apply eqcomm. apply Predindind11. Qed. Lemma revinvolutive: V (A: type). V (l: list A). eq (list A) l (rev A (rev A l)). intro. intro. factorize l. apply listinduc. exact A. simpl. apply eqrefl. intro. intro. intro. simpl. simpl in Predindind11. factorize (rev A (app A (rev A l0) (conc A a (nil A)))). apply eqind. exact (list A). exact (conc A a (rev A (rev A l0))). simpl. factorize (rev A (rev A l0)). apply eqind. exact (list A). exact l0. simpl. apply eqrefl. apply Predindind11. generalize (apprev A (rev A l0) (conc A a (nil A))) as H. simpl. intro. apply eqcomm. exact H. Qed. Lemma revlistind: V (A: type). V (P: V (l: list A). type). V (Pnil: P (nil A)). V (Pconc: V (a: A). V (l: list A). V (Pl: P (rev A l)). P (rev A (conc A a l))). V (l: list A). P (rev A l). intro. intro. intro. intro. intro. factorize l. apply listinduc. exact A. simpl. exact Pnil. simpl. intro. intro. intro. simpl in Pconc. apply Pconc. exact Predindind11. Qed. Lemma revinduc: V (A: type). V (P: V (l: list A). type). V (Pnil: P (nil A)). V (Pconc: V (a: A). V (l: list A). V (Pl: P l). P (app A l (conc A a (nil A)))). V (l: list A). P l. intro. intro. intro. intro. intro. factorize l. apply eqind. exact (list A). exact (rev A (rev A l)). simpl. apply revlistind. apply Pnil. intro. intro. intro. simpl. apply Pconc. apply Pl. apply eqcomm. apply revinvolutive. Qed. Extract Def.