(* EXO 1 *)

Section Exo1.

Inductive pair : nat -> Prop :=
| pair_0 : pair 0
| pair_s2 : forall x, pair x -> pair (S (S x)).

Check pair_ind.

Inductive impair : nat -> Prop := (* ... *)

Lemma spi : forall x, pair x -> impair (S x).
Proof.
(* ... *)
Qed.

Lemma sip : forall x, impair x -> pair (S x).
Proof.
(* ... *)
Qed.

Lemma poui : forall x, pair x \/ impair x.
Proof.
(* ... *)
Qed.

End Exo1.



(* Exo 2 *)

Section Exo2.

Variable char : Set.
Variable a : char.
Variable b : char.

Require Import List.
Definition word : Set := list char.

Definition pempty (w:word) : Prop := (w = nil).
Definition pchar (c:char) (w:word) : Prop := (w = c::nil).

Definition pconcat (p1:word -> Prop) (p2:word -> Prop) (w : word):= (* ... *)

Theorem pconcat_empty : forall p w, pconcat p pempty w -> p w.
Proof.
(* ... *)
Qed.

Inductive pstar (p:word -> Prop) : word -> Prop := 
(* ... *)

Theorem star_concat :
  forall (p:word->Prop) w1 w2,  p w1 -> pstar p w2 -> pstar p (app w1 w2).
Proof.
(* ... *)
Qed.

Theorem concat_star :
  forall (p:word->Prop) w1 w2,  pstar p w1 -> p w2 -> pstar p (app w1 w2).
Proof.
(* ... *)
Qed.

Theorem star_pconcat : 
  forall (p:word->Prop) w, pconcat (pstar p) p w -> pstar p w.
(* ... *)
Qed.

End Exo2.