Commit 83f4dee5 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Realize list.Permut for Coq.

parent 2a4920e2
......@@ -868,7 +868,7 @@ COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map Occ MapPermut MapInjection
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut
COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
COQLIBS_OPTION_FILES = Option
......
......@@ -7,98 +7,47 @@ Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.NumOcc.
Require list.Permut.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted nil)
| Sorted_One : forall (x:Z), (sorted (cons x nil))
Inductive sorted: (list Z) -> Prop :=
| Sorted_Nil : (sorted Init.Datatypes.nil)
| Sorted_One : forall (x:Z), (sorted
(Init.Datatypes.cons x Init.Datatypes.nil))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z -> ((sorted
(cons y l)) -> (sorted (cons x (cons y l)))).
(Init.Datatypes.cons y l)) -> (sorted
(Init.Datatypes.cons x (Init.Datatypes.cons y l)))).
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (list.Mem.mem y
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (cons x l)).
Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)),
match l with
| nil => ((num_occ x l) = 0%Z)
| (cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
end.
Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) <-> (0%Z < (num_occ x l))%Z.
Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), ((num_occ x (List.app l1 l2)) = ((num_occ x
l1) + (num_occ x l2))%Z).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
(permut l l).
Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> (permut l2 l1).
Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
l1 l3)).
Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> (permut (cons x l1)
(cons x l2)).
Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(l:(list a)), (permut (cons x (cons y l)) (cons y (cons x l))).
Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut (List.app (cons x l1) l2)
(List.app l1 (cons x l2))).
Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut (List.app (List.app l1 l2) l3)
(List.app l1 (List.app l2 l3))).
Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
k2) -> (permut (List.app l1 l2) (List.app k1 k2))).
Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (permut (List.app l1 l2)
(List.app l2 l1)).
Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) ->
(list.Mem.mem x l2)).
Axiom Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) ->
((list.Length.length l1) = (list.Length.length l2)).
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (Init.Datatypes.cons x l)).
Import Permut.
(* Why3 goal *)
Theorem WP_parameter_merge : forall (l1:(list Z)) (l2:(list Z)), ((sorted
l1) /\ (sorted l2)) ->
match l2 with
| (cons x x1) =>
| (Init.Datatypes.cons x x1) =>
match l1 with
| (cons x2 x3) => (~ (x2 <= x)%Z) -> (((sorted l1) /\ (sorted x1)) ->
forall (o:(list Z)), ((sorted o) /\ (permut o (List.app l1 x1))) ->
(permut (cons x o) (List.app l1 l2)))
| nil => True
| (Init.Datatypes.cons x2 x3) => (~ (x2 <= x)%Z) -> (((sorted l1) /\
(sorted x1)) -> forall (o:(list Z)), ((sorted o) /\
(list.Permut.permut o (Init.Datatypes.app l1 x1))) ->
(list.Permut.permut (Init.Datatypes.cons x o)
(Init.Datatypes.app l1 l2)))
| Init.Datatypes.nil => True
end
| nil => True
| Init.Datatypes.nil => True
end.
(* Why3 intros l1 l2 (h1,h2). *)
Proof.
intuition.
destruct l2; intuition.
destruct l1; intuition.
......@@ -107,4 +56,3 @@ apply Permut_cons; auto.
apply (Permut_cons_append z).
Qed.
......@@ -7,97 +7,46 @@ Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.NumOcc.
Require list.Permut.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted nil)
| Sorted_One : forall (x:Z), (sorted (cons x nil))
Inductive sorted: (list Z) -> Prop :=
| Sorted_Nil : (sorted Init.Datatypes.nil)
| Sorted_One : forall (x:Z), (sorted
(Init.Datatypes.cons x Init.Datatypes.nil))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z -> ((sorted
(cons y l)) -> (sorted (cons x (cons y l)))).
(Init.Datatypes.cons y l)) -> (sorted
(Init.Datatypes.cons x (Init.Datatypes.cons y l)))).
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (list.Mem.mem y
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (cons x l)).
Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)),
match l with
| nil => ((num_occ x l) = 0%Z)
| (cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
end.
Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) <-> (0%Z < (num_occ x l))%Z.
Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), ((num_occ x (List.app l1 l2)) = ((num_occ x
l1) + (num_occ x l2))%Z).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
(permut l l).
Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> (permut l2 l1).
Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
l1 l3)).
Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> (permut (cons x l1)
(cons x l2)).
Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(l:(list a)), (permut (cons x (cons y l)) (cons y (cons x l))).
Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut (List.app (cons x l1) l2)
(List.app l1 (cons x l2))).
Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut (List.app (List.app l1 l2) l3)
(List.app l1 (List.app l2 l3))).
Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
k2) -> (permut (List.app l1 l2) (List.app k1 k2))).
Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (permut (List.app l1 l2)
(List.app l2 l1)).
Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) ->
(list.Mem.mem x l2)).
Axiom Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) ->
((list.Length.length l1) = (list.Length.length l2)).
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (Init.Datatypes.cons x l)).
Import Permut.
(* Why3 goal *)
Theorem WP_parameter_mergesort : forall (l:(list Z)),
match l with
| (nil|(cons _ nil)) => True
| (Init.Datatypes.nil|(Init.Datatypes.cons _ Init.Datatypes.nil)) => True
| _ => (2%Z <= (list.Length.length l))%Z -> forall (result:(list Z))
(result1:(list Z)), ((1%Z <= (list.Length.length result))%Z /\
((1%Z <= (list.Length.length result1))%Z /\ (permut l
(List.app result result1)))) -> forall (o:(list Z)), ((sorted o) /\
(permut o result1)) -> forall (o1:(list Z)), ((sorted o1) /\ (permut o1
result)) -> (((sorted o1) /\ (sorted o)) -> forall (result2:(list Z)),
((sorted result2) /\ (permut result2 (List.app o1 o))) -> (permut
result2 l))
((1%Z <= (list.Length.length result1))%Z /\ (list.Permut.permut l
(Init.Datatypes.app result result1)))) -> forall (o:(list Z)), ((sorted
o) /\ (list.Permut.permut o result1)) -> forall (o1:(list Z)), ((sorted
o1) /\ (list.Permut.permut o1 result)) -> (((sorted o1) /\ (sorted
o)) -> forall (result2:(list Z)), ((sorted result2) /\
(list.Permut.permut result2 (Init.Datatypes.app o1 o))) ->
(list.Permut.permut result2 l))
end.
(* Why3 intros l. *)
Proof.
destruct l; try trivial.
destruct l; try trivial.
intuition.
......@@ -107,4 +56,3 @@ apply Permut_append; auto.
apply Permut_sym; auto.
Qed.
......@@ -7,87 +7,31 @@ Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.NumOcc.
Require list.Permut.
(* Why3 assumption *)
Definition unit := unit.
Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)),
match l with
| nil => ((num_occ x l) = 0%Z)
| (cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
end.
Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) <-> (0%Z < (num_occ x l))%Z.
Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), ((num_occ x (List.app l1 l2)) = ((num_occ x
l1) + (num_occ x l2))%Z).
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
(permut l l).
Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> (permut l2 l1).
Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
l1 l3)).
Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> (permut (cons x l1)
(cons x l2)).
Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(l:(list a)), (permut (cons x (cons y l)) (cons y (cons x l))).
Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut (List.app (cons x l1) l2)
(List.app l1 (cons x l2))).
Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut (List.app (List.app l1 l2) l3)
(List.app l1 (List.app l2 l3))).
Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
k2) -> (permut (List.app l1 l2) (List.app k1 k2))).
Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (permut (List.app l1 l2)
(List.app l2 l1)).
Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) ->
(list.Mem.mem x l2)).
Axiom Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) ->
((list.Length.length l1) = (list.Length.length l2)).
(* Why3 assumption *)
Inductive t (a:Type) {a_WT:WhyType a} :=
Inductive t (a:Type) :=
| mk_t : (list a) -> t a.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Implicit Arguments mk_t [[a] [a_WT]].
Implicit Arguments mk_t [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (list a) :=
Definition elts {a:Type} {a_WT:WhyType a} (v:(t a)): (list a) :=
match v with
| (mk_t x) => x
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (q:(@t a a_WT)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (q:(t a)): Z :=
(list.Length.length (elts q)).
Axiom elt : Type.
......@@ -102,38 +46,48 @@ Axiom total_preorder2 : forall (x:elt) (y:elt) (z:elt), (le x y) -> ((le y
z) -> (le x z)).
(* Why3 assumption *)
Inductive sorted : (list elt) -> Prop :=
| Sorted_Nil : (sorted nil)
| Sorted_One : forall (x:elt), (sorted (cons x nil))
Inductive sorted: (list elt) -> Prop :=
| Sorted_Nil : (sorted Init.Datatypes.nil)
| Sorted_One : forall (x:elt), (sorted
(Init.Datatypes.cons x Init.Datatypes.nil))
| Sorted_Two : forall (x:elt) (y:elt) (l:(list elt)), (le x y) -> ((sorted
(cons y l)) -> (sorted (cons x (cons y l)))).
(Init.Datatypes.cons y l)) -> (sorted
(Init.Datatypes.cons x (Init.Datatypes.cons y l)))).
Axiom sorted_mem : forall (x:elt) (l:(list elt)), ((forall (y:elt),
(list.Mem.mem y l) -> (le x y)) /\ (sorted l)) <-> (sorted (cons x l)).
(list.Mem.mem y l) -> (le x y)) /\ (sorted l)) <-> (sorted
(Init.Datatypes.cons x l)).
Import Permut.
(* Why3 goal *)
Theorem WP_parameter_merge : forall (q:(list elt)) (q2:(list elt))
(q1:(list elt)), (q = nil) -> forall (q3:(list elt)) (q21:(list elt))
(q11:(list elt)), (permut (List.app (List.app q3 q11) q21)
(List.app q1 q2)) -> ((0%Z < (list.Length.length q11))%Z ->
Theorem WP_parameter_merge : forall (q1:(list elt)) (q2:(list elt))
(q:(list elt)), (q = Init.Datatypes.nil) -> forall (q3:(list elt))
(q21:(list elt)) (q11:(list elt)), (list.Permut.permut
(Init.Datatypes.app (Init.Datatypes.app q3 q11) q21)
(Init.Datatypes.app q1 q2)) -> ((0%Z < (list.Length.length q11))%Z ->
((~ ((list.Length.length q11) = 0%Z)) ->
((~ ((list.Length.length q21) = 0%Z)) -> ((~ (q11 = nil)) ->
forall (x1:elt), match q11 with
| nil => False
| (cons x _) => (x1 = x)
end -> ((~ (q21 = nil)) -> forall (x2:elt),
((~ ((list.Length.length q21) = 0%Z)) -> ((~ (q11 = Init.Datatypes.nil)) ->
forall (x1:elt),
match q11 with
| Init.Datatypes.nil => False
| (Init.Datatypes.cons x _) => (x1 = x)
end -> ((~ (q21 = Init.Datatypes.nil)) -> forall (x2:elt),
match q21 with
| nil => False
| (cons x _) => (x2 = x)
end -> ((~ (le x1 x2)) -> ((~ (q21 = nil)) -> forall (q22:(list elt)),
forall (o:elt),
| Init.Datatypes.nil => False
| (Init.Datatypes.cons x _) => (x2 = x)
end -> ((~ (le x1 x2)) -> ((~ (q21 = Init.Datatypes.nil)) ->
forall (q22:(list elt)), forall (o:elt),
match q21 with
| nil => False
| (cons x t1) => (o = x) /\ (q22 = t1)
end -> forall (q4:(list elt)), (q4 = (List.app q3 (cons o nil))) -> (permut
(List.app (List.app q4 q11) q22) (List.app q1 q2))))))))).
(* Why3 intros q q2 q1 h1 q3 q21 q11 h2 h3 h4 h5 h6 x1 h7 h8 x2 h9 h10 h11
| Init.Datatypes.nil => False
| (Init.Datatypes.cons x t1) => (o = x) /\ (q22 = t1)
end -> forall (q4:(list elt)),
(q4 = (Init.Datatypes.app q3 (Init.Datatypes.cons o Init.Datatypes.nil))) ->
(list.Permut.permut (Init.Datatypes.app (Init.Datatypes.app q4 q11) q22)
(Init.Datatypes.app q1 q2))))))))).
(* Why3 intros q1 q2 q h1 q3 q21 q11 h2 h3 h4 h5 h6 x1 h7 h8 x2 h9 h10 h11
q22 o h12 q4 h13. *)
Proof.
intros q q2 q1 h1 q3 q21 q11 h2 h3 h4 h5 h6 x1 h7 x2 h8 h9 q22 o h10
q4 h11.
destruct q21.
......@@ -147,4 +101,3 @@ simpl.
apply (Permut_cons_append e).
Qed.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.NumOcc.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((list.NumOcc.num_occ x
l1) = (list.NumOcc.num_occ x l2)).
(* Why3 goal *)
Lemma Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
(permut l l).
Proof.
now intros a a_WT l.
Qed.
(* Why3 goal *)
Lemma Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> (permut l2 l1).
Proof.
now intros a a_WT l1 l2 h1.
Qed.
(* Why3 goal *)
Lemma Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
l1 l3)).
Proof.
intros a a_WT l1 l2 l3 h1 h2 x.
now rewrite h1.
Qed.
(* Why3 goal *)
Lemma Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> (permut
(Init.Datatypes.cons x l1) (Init.Datatypes.cons x l2)).
Proof.
intros a a_WT x l1 l2 h1 y.
simpl.
now rewrite h1.
Qed.
(* Why3 goal *)
Lemma Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(l:(list a)), (permut (Init.Datatypes.cons x (Init.Datatypes.cons y l))
(Init.Datatypes.cons y (Init.Datatypes.cons x l))).
Proof.
intros a a_WT x y l z.
simpl.
ring.
Qed.
(* Why3 goal *)
Lemma Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut
(Init.Datatypes.app (Init.Datatypes.cons x l1) l2)
(Init.Datatypes.app l1 (Init.Datatypes.cons x l2))).
Proof.
intros a a_WT x l1 l2 y.
induction l1 as [|l1h l1t IHl1].
easy.
simpl in IHl1 |- *.
rewrite <- IHl1.
ring.
Qed.
(* Why3 goal *)
Lemma Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut
(Init.Datatypes.app (Init.Datatypes.app l1 l2) l3)
(Init.Datatypes.app l1 (Init.Datatypes.app l2 l3))).
Proof.
intros a a_WT l1 l2 l3 y.
now rewrite List.app_assoc.
Qed.
(* Why3 goal *)
Lemma Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
k2) -> (permut (Init.Datatypes.app l1 l2) (Init.Datatypes.app k1 k2))).
Proof.
intros a a_WT l1 l2 k1 k2 h1 h2 y.
rewrite 2!NumOcc.Append_Num_Occ.
now apply f_equal2.
Qed.
(* Why3 goal *)
Lemma Permut_append_swap : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (permut (Init.Datatypes.app l1 l2)
(Init.Datatypes.app l2 l1)).
Proof.
intros a a_WT l1 l2 y.
rewrite 2!NumOcc.Append_Num_Occ.
apply Zplus_comm.
Qed.
(* Why3 goal *)
Lemma Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) ->
(list.Mem.mem x l2)).
Proof.
intros a a_WT x l1 l2 h1 h2.
apply NumOcc.Mem_Num_Occ.
rewrite <- h1.
now apply NumOcc.Mem_Num_Occ.
Qed.
(* Why3 goal *)
Lemma Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) ->
((list.Length.length l1) = (list.Length.length l2)).
Proof.
intros a a_WT l1 l2 h1.
revert l2 h1.
induction l1 as [|l1h l1t IHl1].
- destruct l2 as [|l2h l2t].
easy.
intros H.
specialize (H l2h).
contradict H.
simpl.
case why_decidable_eq ; intros H.
generalize (NumOcc.Num_Occ_pos l2h l2t).
omega.
now elim H.
- intros l2 H.
assert (H': Mem.mem l1h l2).
apply NumOcc.Mem_Num_Occ.
specialize (H l1h).
simpl in H.
destruct (why_decidable_eq l1h l1h) as [_|H'].
2: now elim H'.
generalize (NumOcc.Num_Occ_pos l1h l1t).
omega.
destruct (Append.mem_decomp _ _ H') as [l2a [l2b Hl2]].
rewrite Hl2.
rewrite Append.Append_length.
change (1 + Length.length l1t = Length.length l2a + (1 + Length.length l2b))%Z.
rewrite (IHl1 (l2a ++ l2b)%list).
rewrite Append.Append_length.
ring.
rewrite Hl2 in H.
assert (H1 := Permut_cons_append l1h l2a l2b).
apply Permut_sym in H1.
generalize (Permut_trans _ _ _ H H1).
change ((l1h :: l2a) ++ l2b)%list with (l1h :: (l2a ++ l2b))%list.
generalize (l2a ++ l2b)%list.
clear.
intros l H y.
specialize (H y).
simpl in H.
omega.
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment