124 lines
2.8 KiB
Coq
Executable file
124 lines
2.8 KiB
Coq
Executable file
Require Import Extraction.
|
||
(* Ouverture d’une section *)
|
||
Section Induction.
|
||
(* Déclaration d’un domaine pour les éléments des listes *)
|
||
Variable A : Set.
|
||
|
||
Inductive liste : Set :=
|
||
Nil : liste
|
||
| Cons : A -> liste -> liste.
|
||
|
||
(* Déclaration du nom de la fonction *)
|
||
Variable append_spec : liste -> liste -> liste.
|
||
|
||
(* Spécification du comportement pour Nil *)
|
||
Axiom append_Nil : forall (l : liste), append_spec Nil l = l.
|
||
|
||
(* Spécification du comportement pour Cons *)
|
||
Axiom append_Cons : forall (t : A), forall (q l : liste),
|
||
append_spec (Cons t q) l = Cons t (append_spec q l).
|
||
|
||
Theorem append_Nil_right : forall (l : liste), (append_spec l Nil) = l.
|
||
intros.
|
||
induction l.
|
||
(* cas de base *)
|
||
apply append_Nil.
|
||
(* cas général *)
|
||
rewrite append_Cons.
|
||
rewrite IHl.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
|
||
Theorem append_associative : forall (l1 l2 l3 : liste),
|
||
(append_spec l1 (append_spec l2 l3)) = (append_spec (append_spec l1 l2) l3).
|
||
intros.
|
||
induction l1.
|
||
(* cas de base *)
|
||
rewrite append_Nil.
|
||
rewrite append_Nil.
|
||
reflexivity.
|
||
(* cas général *)
|
||
rewrite append_Cons.
|
||
rewrite append_Cons.
|
||
rewrite append_Cons.
|
||
rewrite IHl1.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
|
||
(* Implantation de la fonction append *)
|
||
Fixpoint append_impl (l1 l2 : liste) {struct l1} : liste :=
|
||
match l1 with
|
||
Nil => l2
|
||
| (Cons t1 q1) => (Cons t1 (append_impl q1 l2))
|
||
end.
|
||
|
||
Theorem append_correctness : forall (l1 l2 : liste),
|
||
(append_spec l1 l2) = (append_impl l1 l2).
|
||
intros.
|
||
induction l1.
|
||
(* cas de base *)
|
||
rewrite append_Nil.
|
||
simpl append_impl.
|
||
reflexivity.
|
||
(* cas général *)
|
||
rewrite append_Cons.
|
||
simpl append_impl.
|
||
rewrite IHl1.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
(* Implantation de la fonction rev (reverse d'une liste) *)
|
||
Fixpoint rev_impl (l : liste) : liste :=
|
||
match l with
|
||
Nil => l
|
||
| (Cons x y) => ( append_impl (rev_impl y) (Cons x Nil) )
|
||
end.
|
||
|
||
|
||
Lemma rev_append : forall (l1 l2 : liste),
|
||
(rev_impl (append_impl l1 l2)) = (append_impl (rev_impl l2) (rev_impl l1)).
|
||
intros.
|
||
induction l1.
|
||
(* cas de base *)
|
||
simpl rev_impl.
|
||
rewrite <- append_correctness.
|
||
rewrite append_Nil_right.
|
||
reflexivity.
|
||
(* cas général *)
|
||
simpl rev_impl.
|
||
rewrite IHl1.
|
||
rewrite <- append_correctness.
|
||
rewrite <- append_correctness.
|
||
rewrite <- append_correctness.
|
||
rewrite <- append_correctness.
|
||
rewrite append_associative.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
Theorem rev_rev : forall (l : liste), (rev_impl (rev_impl l)) = l.
|
||
intros.
|
||
induction l.
|
||
(* cas de base *)
|
||
simpl rev_impl.
|
||
reflexivity.
|
||
(* cas général *)
|
||
simpl rev_impl.
|
||
rewrite rev_append.
|
||
rewrite IHl.
|
||
simpl rev_impl.
|
||
rewrite <- append_correctness.
|
||
rewrite append_Cons.
|
||
rewrite append_Nil.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
End Induction.
|
||
Extraction Language Ocaml.
|
||
Extraction "/tmp/induction" append_impl rev_impl.
|
||
Extraction Language Haskell.
|
||
Extraction "/tmp/induction" append_impl rev_impl.
|
||
Extraction Language Scheme.
|
||
Extraction "/tmp/induction" append_impl rev_impl.
|