Append.v 1.94 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
(* 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.

(* Why3 goal *)
Lemma infix_plpl_def  {a:Type} {a_WT:WhyType a}: forall (l1:(list a))
  (l2:(list a)),
  ((List.app l1 l2) = match l1 with
  | nil => l2
  | (cons x1 r1) => (cons x1 (List.app r1 l2))
  end).
Proof.
now intros [|h1 q1] l2.
Qed.

Require Import Lists.List.

(* Why3 goal *)
Lemma Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
  (l2:(list a)) (l3:(list a)),
  ((List.app l1 (List.app l2 l3)) = (List.app (List.app l1 l2) l3)).
Proof.
intros a a_WT l1 l2 l3.
apply app_assoc.
Qed.

(* Why3 goal *)
Lemma Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
  ((List.app l nil) = l).
Proof.
intros a a_WT l.
apply app_nil_r.
Qed.

(* Why3 goal *)
Lemma Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
  (l2:(list a)),
  ((list.Length.length (List.app l1 l2)) = ((list.Length.length l1) + (list.Length.length l2))%Z).
Proof.
intros a a_WT l1 l2.
rewrite 3!Length.length_std.
now rewrite app_length, inj_plus.
Qed.

(* Why3 goal *)
Lemma mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (l1:(list a)) (l2:(list a)), (list.Mem.mem x (List.app l1 l2)) <->
  ((list.Mem.mem x l1) \/ (list.Mem.mem x l2)).
Proof.
intros a a_WT x l1 l2.
split.
intros H.
apply Mem.mem_std in H.
apply in_app_or in H.
destruct H as [H|H].
left.
now apply Mem.mem_std.
right.
now apply Mem.mem_std.
intros H.
apply Mem.mem_std.
apply in_or_app.
destruct H as [H|H].
left.
now apply Mem.mem_std.
right.
now apply Mem.mem_std.
Qed.

(* Why3 goal *)
Lemma mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (l:(list a)), (list.Mem.mem x l) -> exists l1:(list a), exists l2:(list a),
  (l = (List.app l1 (cons x l2))).
Proof.
intros a a_WT x l h1.
apply in_split.
now apply Mem.mem_std.
Qed.