124 lines
2.8 KiB
Coq
124 lines
2.8 KiB
Coq
|
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.
|