(* 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.