val push_as_map (ss1 ss2:ss_t)
  : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
          (ensures as_map (push_ss ss1 ss2) == Map.concat (as_map ss1) (as_map ss2))
          [SMTPat (as_map (push_ss ss1 ss2))]
let push_as_map (ss1 ss2:ss_t)
  : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
          (ensures Map.equal (as_map (push_ss ss1 ss2))
                             (Map.concat (as_map ss1) (as_map ss2)))
          (decreases L.length ss2.l)
          [SMTPat (as_map (push_ss ss1 ss2))] =

  let rec aux (ss1 ss2:ss_t)
    : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
            (ensures Map.equal (as_map (push_ss ss1 ss2))
                               (Map.concat (as_map ss1) (as_map ss2)))
            (decreases L.length ss2.l)
            [SMTPat ()] =
    match ss2.l with
    | [] -> ()
    | x::tl -> aux (push ss1 x (Map.sel ss2.m x)) (tail ss2)
  in
  ()
val push_as_map (ss1 ss2:ss_t)
  : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
          (ensures as_map (push_ss ss1 ss2) == Map.concat (as_map ss1) (as_map ss2))
          [SMTPat (as_map (push_ss ss1 ss2))]
let push_as_map (ss1 ss2: ss_t)
    : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
      (ensures Map.equal (as_map (push_ss ss1 ss2)) (Map.concat (as_map ss1) (as_map ss2)))
      (decreases L.length ss2.l)
      [SMTPat (as_map (push_ss ss1 ss2))] =
let rec aux (ss1 ss2: ss_t)
    : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
      (ensures Map.equal (as_map (push_ss ss1 ss2)) (Map.concat (as_map ss1) (as_map ss2)))
      (decreases L.length ss2.l)
      [SMTPat ()] =
  match ss2.l with
  | [] -> ()
  | x :: tl -> aux (push ss1 x (Map.sel ss2.m x)) (tail ss2)
in
()
Pulse.Checker.Prover.Substs.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.IndefiniteDescription.fsti.checked
Pulse.Checker.Prover.Substs.fst
Pulse.Checker.Prover.Substs.ss_t Prims.unit FStar.List.Tot.Base.length Pulse.Syntax.Base.var Pulse.Checker.Prover.Substs.__proj__Mkss_t__item__l FStar.Set.disjoint Pulse.Checker.Prover.Substs.dom Prims.squash FStar.Map.equal Pulse.Syntax.Base.term Pulse.Checker.Prover.Substs.as_map Pulse.Checker.Prover.Substs.push_ss FStar.Map.concat Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil Prims.list Pulse.Checker.Prover.Substs.push FStar.Map.sel Pulse.Checker.Prover.Substs.__proj__Mkss_t__item__m Pulse.Checker.Prover.Substs.tail FStar.Map.t
module Pulse.Checker.Prover.Substs

open FStar.List.Tot

open Pulse.Syntax
open Pulse.Typing.Env
open Pulse.Typing

module L = FStar.List.Tot
module Env = Pulse.Typing.Env
module Metatheory = Pulse.Typing.Metatheory

let coerce_eq (#a #b:Type) (x:a) (_:squash (a == b)) : y:b {y == x} = x

let rec no_repeats (l:list var) : Type0 =
  match l with
  | [] -> True
  | x::tl -> (~ (L.memP x tl)) /\ no_repeats tl  

type ss_dom = l:list var { no_repeats l }

type ss_map = m:Map.t var term {
  forall (x:var). (~ (Map.contains m x)) ==> Map.sel m x == tm_unknown
}

let remove_map (m:ss_map) (x:var) =
  Map.restrict (Set.complement (Set.singleton x)) (Map.upd m x tm_unknown)

let rec is_dom (l:ss_dom) (m:ss_map) : Type0 =
  match l with
  | [] -> Set.equal (Map.domain m) Set.empty
  | x::tl ->
    Map.contains m x /\ is_dom tl (remove_map m x)

let rec is_dom_mem (l:ss_dom) (m:ss_map)
  : Lemma
      (requires is_dom l m)
      (ensures forall (x:var).{:pattern L.memP x l \/ Map.contains m x}
                              L.memP x l <==> Map.contains m x)
      [SMTPat (is_dom l m)] =
  match l with
  | [] -> ()
  | y::tl -> is_dom_mem tl (remove_map m y)

noeq
type ss_t = {
  l : ss_dom;
  m : m:ss_map { is_dom l m }
}

let as_map (ss:ss_t) = ss.m

let empty = { l = []; m = Map.const_on Set.empty tm_unknown }

let is_dom_push
  (l:ss_dom)
  (m:ss_map { is_dom l m })
  (x:var { ~ (Map.contains m x ) })
  (t:term)
  : Lemma (is_dom (x::l) (Map.upd m x t)) =

  assert (Map.equal (remove_map (Map.upd m x t) x) m)

let push (ss:ss_t) (x:var { ~ (contains ss x) }) (t:term) : ss_t =
  
  is_dom_push ss.l ss.m x t;
  { l = x::ss.l;
    m = Map.upd ss.m x t }

let tail (ss:ss_t { Cons? ss.l }) : ss_t =
   { l = L.tl ss.l; m = remove_map ss.m (L.hd ss.l) }

let rec push_ss (ss1:ss_t) (ss2:ss_t { Set.disjoint (dom ss1) (dom ss2) })
  : Tot ss_t (decreases L.length ss2.l) =
  match ss2.l with
  | [] -> ss1
  | x::tl ->
    push_ss (push ss1 x (Map.sel ss2.m x)) (tail ss2)

let check_disjoint ss1 ss2 =
  admit ();
  not (L.existsb (fun v1 -> L.mem v1 ss2.l) ss1.l)

#push-options "--warn_error -271"
let push_as_map (ss1 ss2:ss_t)
  : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
          (ensures Map.equal (as_map (push_ss ss1 ss2))
                             (Map.concat (as_map ss1) (as_map ss2)))
val push_as_map (ss1 ss2:ss_t)
  : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
          (ensures as_map (push_ss ss1 ss2) == Map.concat (as_map ss1) (as_map ss2))
          [SMTPat (as_map (push_ss ss1 ss2))]
ss1: Pulse.Checker.Prover.Substs.ss_t -> ss2: Pulse.Checker.Prover.Substs.ss_t
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Set.disjoint (Pulse.Checker.Prover.Substs.dom ss1)
          (Pulse.Checker.Prover.Substs.dom ss2))
      (ensures
        Pulse.Checker.Prover.Substs.as_map (Pulse.Checker.Prover.Substs.push_ss ss1 ss2) ==
        FStar.Map.concat (Pulse.Checker.Prover.Substs.as_map ss1)
          (Pulse.Checker.Prover.Substs.as_map ss2))
      [SMTPat (Pulse.Checker.Prover.Substs.as_map (Pulse.Checker.Prover.Substs.push_ss ss1 ss2))]