theory Distincts
  use int.Int
  use seq.Seq
  use seq.Occ
  use seq.FreeMonoid
  use proofs.lib.seq.Seq

  type t

  predicate distinct (x y : t)

  axiom distinct_sym : forall x y. distinct x y <-> distinct y x
  axiom distinct_irreflexive : forall x. not distinct x x
  axiom distinct_imp_diff : forall x y. distinct x y -> x <> y

  predicate all_distincts (s : seq t) =
    seq_forall_two distinct s

  lemma alld_sub: forall x : t, s : seq t.
    all_distincts (cons x s) -> all_distincts s

  lemma alld_append:
    forall s1 s2.
    (all_distincts s1 /\ all_distincts s2 /\
      (forall i j: int. 0 <= i < length s1 /\ 0 <= j < length s2 ->
       distinct s1[i] s2[j])) <-> all_distincts (s1 ++ s2)

  let lemma alld_inst (s : seq t) ( i j : int)
  requires { 0 <= i < length s }
  requires { 0 <= j < length s }
  requires { i <> j }
  requires { all_distincts s }
  ensures { distinct s[i] s[j] }
  =
  ()

  lemma alld_comm:
    forall s1, s2: seq t.
    all_distincts (s1 ++ s2) <-> all_distincts (s2 ++ s1)

  lemma alld_cons:
    forall x: t, s: seq t.
    all_distincts s ->
    (seq_forall (distinct x) s) <-> all_distincts (cons x s)

  lemma alld_snoc:
    forall x: t, s: seq t.
    (seq_forall (distinct x) s /\ all_distincts s) <-> all_distincts (snoc s x)

  let lemma alld_snoc2  (s1 s2 s3 : seq t)
    requires { all_distincts (s1 ++ s2 ++ s3) }
    requires { s1 <> empty }
    ensures { all_distincts (s1[1..] ++ s2 ++ (snoc s3 s1[0])) }
    ensures { all_distincts (s2 ++ s1[1..] ++ (snoc s3 s1[0])) }
  =
    assert { all_distincts (snoc s3 s1[0]) };
    assert { all_distincts (s1[1..] ++ (snoc s3 s1[0])) };
    assert { all_distincts (s2 ++ (snoc s3 s1[0])) };
    assert { all_distincts (s1[1..] ++ (s2 ++ (snoc s3 s1[0]))) };
    assert { all_distincts (s2 ++ (s1[1..] ++ (snoc s3 s1[0]))) };

  lemma alld_mv:
    forall x: t, s1: seq t, s2: seq t.
    all_distincts ((cons x s1) ++ s2) -> all_distincts (s1 ++ (cons x s2))

  (* lemma alld_mvt: *)
  (*   forall b: seq t, nb: seq t, oa: seq t. *)
  (*   b <> empty -> *)
  (*    all_distincts (b ++ oa) /\ *)
  (*    all_distincts (b ++ nb) /\ *)
  (*    all_distincts (nb ++ oa) -> *)
  (*    all_distincts (cons b[0] oa) /\ *)
  (*    all_distincts (nb ++ (cons b[0] oa)) *)

  let lemma alld_mvt (b nb oa : seq t)
    requires { b <> empty }
    requires { all_distincts (b ++ oa) }
    requires { all_distincts (b ++ nb) }
    requires { all_distincts (nb ++ oa) }
    ensures { all_distincts (cons b[0] oa) }
    ensures { all_distincts (nb ++ (cons b[0] oa)) }
  = ()

  lemma alld_dd:
    forall a, b, c: seq t.
    all_distincts (a ++ b) /\
    all_distincts (b ++ c) /\
    all_distincts (c ++ a)
    <->
    all_distincts (a ++ b ++ c)

  let lemma alld_app (s1 s2 : seq t)
    requires { all_distincts (s1 ++ s2) }
    ensures { forall i j: int. 0 <= i < length s1 -> 0 <= j < length s2 ->
              distinct s1[i] s2[j] }
  = ()

  let lemma alld_prop (s : seq t) (i j : int) (p : t -> t -> bool)
    requires { forall x y. distinct x y <-> p x y }
    requires { all_distincts s }
    requires { 0 <= i < length s }
    requires { 0 <= j < length s }
    requires { i <> j }
    ensures { p s[i] s[j] }
  = ()

  let rec lemma alld_occ (s : seq t)
    requires { all_distincts s }
    ensures { forall i. 0 <= i < length s -> occ_all s[i] s = 1 }
    variant { length s }
  =
    if length s = 0 then return;
    alld_occ s[1..];
    if occ_all s[0] s[1..] > 0 then begin
      let sp = s[1..] in
      let j = any (j : int) ensures { 0 <= j < length sp && sp[j] = s[0] } in
      assert { not distinct s[0] s[j+1] };
      absurd;
    end

  let lemma alld_cons_suffix (s1 s2 : seq t) (i : int)
    requires { 0 <= i < length s2 }
    requires { forall j. 0 <= j < length s1 -> seq_forall (distinct s1[j]) s2[i..] }
    requires { all_distincts s1 }
    ensures { forall j. 0 <= j < length s1 -> distinct s1[j] s2[i] }
    ensures { all_distincts (snoc s1 s2[i]) }
  =
    ()
end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)