Commit 429990f3 authored by MARCHE Claude's avatar MARCHE Claude

Fixed Coq realizations of list.why

parent a4f368c0
......@@ -38,9 +38,9 @@ change ((if why_decidable_eq x y then 1 else 0) + num_occ x r = 0 + num_occ x r)
now case why_decidable_eq.
Qed.
Lemma Num_Occ_pos : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (0 <= (num_occ x l))%Z.
Proof.
(* Why3 goal *)
Lemma Num_Occ_NonNeg : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (0%Z <= (num_occ x l))%Z.
intros a a_WT x l.
induction l as [|lh lt IHl].
easy.
......@@ -61,7 +61,7 @@ simpl.
case why_decidable_eq ; intros H ; split.
intros _.
clear.
generalize (Num_Occ_pos x lt).
generalize (Num_Occ_NonNeg x lt).
omega.
now left.
intros [H'|H'] ; try easy.
......
......@@ -128,7 +128,7 @@ induction l1 as [|l1h l1t IHl1].
contradict H.
simpl.
case why_decidable_eq ; intros H.
generalize (NumOcc.Num_Occ_pos l2h l2t).
generalize (NumOcc.Num_Occ_NonNeg l2h l2t).
omega.
now elim H.
- intros l2 H.
......@@ -138,7 +138,7 @@ induction l1 as [|l1h l1t IHl1].
simpl in H.
destruct (why_decidable_eq l1h l1h) as [_|H'].
2: now elim H'.
generalize (NumOcc.Num_Occ_pos l1h l1t).
generalize (NumOcc.Num_Occ_NonNeg l1h l1t).
omega.
destruct (Append.mem_decomp _ _ H') as [l2a [l2b Hl2]].
rewrite Hl2.
......
......@@ -32,20 +32,6 @@ easy.
now simpl.
Qed.
(* Why3 goal *)
Lemma rev_append_append_r : forall {a:Type} {a_WT:WhyType a},
forall (r:(list a)) (s:(list a)) (t:(list a)),
((Lists.List.rev_append r (Init.Datatypes.app s t)) = (Lists.List.rev_append (Lists.List.rev_append s r) t)).
Proof.
intros a a_WT r s t.
revert r.
induction s as [|sh st IHs].
easy.
intros r.
simpl.
now rewrite <- IHs.
Qed.
(* Why3 goal *)
Lemma rev_append_length : forall {a:Type} {a_WT:WhyType a},
forall (s:(list a)) (t:(list a)),
......@@ -74,3 +60,17 @@ rewrite <- Append.Append_assoc.
simpl. reflexivity.
Qed.
(* Why3 goal *)
Lemma rev_append_append_r : forall {a:Type} {a_WT:WhyType a},
forall (r:(list a)) (s:(list a)) (t:(list a)),
((Lists.List.rev_append r (Init.Datatypes.app s t)) = (Lists.List.rev_append (Lists.List.rev_append s r) t)).
Proof.
intros a a_WT r s t.
revert r.
induction s as [|sh st IHs].
easy.
intros r.
simpl.
now rewrite <- IHs.
Qed.
......@@ -38,6 +38,14 @@ simpl.
auto.
Qed.
(* Why3 goal *)
Lemma cons_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(x:a),
((Init.Datatypes.cons x (Lists.List.rev l)) = (Lists.List.rev (Init.Datatypes.app l (Init.Datatypes.cons x Init.Datatypes.nil)))).
intros a a_WT l x.
now rewrite List.rev_unit.
Qed.
(* Why3 goal *)
Lemma reverse_reverse : forall {a:Type} {a_WT:WhyType a},
forall (l:(list a)), ((Lists.List.rev (Lists.List.rev l)) = l).
......
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