Distinct.v 1.93 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15 16 17 18 19 20
(* 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.
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

(* Why3 assumption *)
Inductive distinct {a:Type} {a_WT:WhyType a}: (list a) -> Prop :=
  | distinct_zero : (distinct Init.Datatypes.nil)
  | distinct_one : forall (x:a), (distinct
      (Init.Datatypes.cons x Init.Datatypes.nil))
  | distinct_many : forall (x:a) (l:(list a)), (~ (list.Mem.mem x l)) ->
      ((distinct l) -> (distinct (Init.Datatypes.cons x l))).

(* Why3 goal *)
Lemma distinct_append : forall {a:Type} {a_WT:WhyType a},
  forall (l1:(list a)) (l2:(list a)), (distinct l1) -> ((distinct l2) ->
  ((forall (x:a), (list.Mem.mem x l1) -> ~ (list.Mem.mem x l2)) -> (distinct
  (Init.Datatypes.app l1 l2)))).
Proof.
intros a a_WT l1 l2 h1 h2 h3.
induction l1 as [|l1h l1t IHl1].
exact h2.
simpl.
inversion h1 ; subst.
- apply distinct_many with (2 := h2).
  apply h3.
  now left.
- apply distinct_many.
  contradict H1.
  apply Append.mem_append in H1.
  destruct H1 as [H1|H1].
  exact H1.
  elim h3 with (2 := H1).
  now left.
  apply IHl1 with (1 := H2).
  intros x Hx.
  apply h3.
  now right.
Qed.