Require Import Coq.Program.Wf.

Require Export stdpp.gmultiset.

Require Import CoLoR.Util.Multiset.MultisetOrder.
Require Import CoLoR.Util.Multiset.MultisetCore.

Require Export Pqf.Formulas.

Definition env := @gmultiset form form_eq_dec form_count.

Global Instance singleton : Singleton form env := gmultiset_singleton.
Global Instance singletonMS : SingletonMS form env := base.singleton.

Module Export EnvMS <: MultisetCore.

  Module Sid <: RelExtras.Eqset_dec.
    Module Export Dom. Definition A : Type := form. End Dom.
    Module Export Eq := Relation.RelExtras.Eqset_def Dom.
    Definition eqA_dec := form_eq_dec.
  End Sid.
  Definition Multiset := env.
  Definition mult : form -> Multiset -> nat := multiplicity.
  Definition meq := (≡@{env}).
  Definition empty := ∅ : env.
  Definition singleton (x : form) : env := {[ x ]}.
  Definition union : env -> env -> env := disj_union.
  Definition intersection : env -> env -> env := intersection.
  Definition diff : env -> env -> env := difference.

  Lemma mult_eqA_compat M x y : (x = y) -> mult x M = mult y M.
  Proof. intro; now subst. Qed.

  Lemma meq_multeq M N:
    M ≡ N -> (forall x, mult x M = mult x N).
  Proof. intro Heq; multiset_solver. Qed.

  Lemma multeq_meq M N: (forall x, mult x M = mult x N) -> M ≡ N.
  Proof. multiset_solver. Qed.

  Lemma empty_mult (x : form): mult x (∅ : env) = 0.
  Proof. multiset_solver. Qed.

  Lemma union_mult M N (x : form) :
    mult x (M ⊎ N) = (mult x M + mult x N)%nat.
  Proof. apply multiplicity_disj_union. Qed.

  Lemma diff_mult M N (x : form):
    mult x (M ∖ N) = (mult x M - mult x N)%nat.
  Proof. apply multiplicity_difference. Qed.

  Lemma intersection_mult (M N : env) (x : form):
    mult x (M ∩ N) = min (mult x M) (mult x N).
  Proof. apply multiplicity_intersection. Qed.

  Lemma singleton_mult_in (x y: form): x = y -> mult x {[y]} = 1.
    intro Heq. rewrite Heq. unfold mult. apply multiplicity_singleton. Qed.

  Lemma singleton_mult_notin (x y: form): x <> y -> mult x {[y]} = 0.
  Proof. apply multiplicity_singleton_ne. Qed.

  (* reprove the following principles, proved in stdpp for Prop, but
     we need them in Type *)
  Lemma gmultiset_choose_or_empty (X : env) : {x | x ∈ X} + {X = ∅}.
  Proof.
    destruct (elements X) as [|x l] eqn:HX; [right|left].
    - by apply gmultiset_elements_empty_inv.
    - exists x. rewrite <- (gmultiset_elem_of_elements x X).
      replace (elements X) with (x :: l). left.
  Qed.

  Definition mset_ind_type : forall P : env -> Type,
        P empty -> (forall M a, P M -> P (M ⊎ {[a]})) -> forall M, P M.
  Proof.
    intros P Hemp Hinsert X.
    eapply (Fix gmultiset_wf _ X).
    Unshelve. clear X. intros X IH.
    destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; try assumption.
    rewrite (gmultiset_disj_union_difference' x X) by done.
    rewrite gmultiset_disj_union_comm.
    apply Hinsert, IH. apply gmultiset_difference_subset;
     multiset_solver.
  Defined.

End EnvMS.

Global Hint Unfold mult meq empty singleton union intersection diff env Sid.Eq.A Sid.Dom.A: mset.

Module Export MO := MultisetOrder EnvMS. (* for the well-foundedness *)

(* useful notations :
  { x } : singleton
      ⊎ : disjoint union
   \: difference (setminus)
   { x; y; … } union of singletons
   {[+ x; y; … +]} *disjoint* union of singletons
      ⊂@ : include
*)

Definition env_order (Γ Δ : env): Prop := MO.MultisetGt form_order Δ Γ.
Infix "≺" := env_order (at level 150).

Global Hint Unfold form_order : mset.
Global Hint Unfold base.singletonMS : mset.
Global Hint Unfold singletonMS : mset.
Ltac ms :=
  unfold base.singletonMS;
  unfold singletonMS; (* necessary, not sure why *)
  autounfold with mset in *;
  autounfold with mset; multiset_solver.

Global Instance proper_elem_of : Proper ((=) ==> (≡@{env}) ==> (fun x y => x <-> y)) elem_of.
Proof. intros Γ Γ' Heq φ φ' Heq'. ms. Qed.

Global Instance proper_disj_union : Proper ((≡@{env}) ==> (≡@{env}) ==> (≡@{env})) disj_union.
Proof. intros Γ Γ' Heq Δ Δ' Heq'. ms. Qed.

(* example of the multiset ordering *)
Local Lemma example_multiset : (forall φ ψ: form, {[ φ; ψ ]} ≺ {[ φ ∧ ψ ]}).
Proof. intros.
constructor. eapply MSetRed with(X:= ∅) (a := φ ∧ ψ) (Y := {[φ; ψ]}).
ms. ms.
intros y Hy.
unfold MSet.member, gt, mult in Hy.
rewrite <- elem_of_multiplicity in Hy. ms.
Qed.

Definition wf_env_order : well_founded env_order.
Proof.
  apply mord_wf.
  - unfold Sid.Eq.eqA. intros s y Heq; now subst.
  - now apply well_founded_lt_compat with (f := weight).
Defined.

Global Notation "Γ • φ" := (disj_union Γ (base.singletonMS φ)) (at level 105, φ at level 85, left associativity).

(* Two useful basic facts about multisets containing (or not) certain elements. *)
Lemma env_replace {Γ : env} φ {ψ : form}:
  (ψ ∈ Γ) -> (Γ • φ) ∖ {[ψ]} ≡ (Γ ∖ {[ψ]} • φ).
Proof.
intro Hin; apply multeq_meq. intros θ.
rewrite diff_mult, union_mult, union_mult, diff_mult.
apply PeanoNat.Nat.add_sub_swap.
case (decide (θ = ψ)); intro; subst.
- now rewrite singleton_mult_in.
- rewrite singleton_mult_notin; trivial. lia.
Qed.

Lemma diff_not_in (Γ : env) φ : φ ∉ Γ -> Γ ∖ {[φ]} ≡ Γ.
Proof.
intro Hf. apply multeq_meq. intros ψ.
rewrite diff_mult. rewrite (elem_of_multiplicity φ Γ) in Hf.
unfold mult.
case (decide (φ = ψ)).
- intro; subst. lia.
- intro Hneq. setoid_rewrite (multiplicity_singleton_ne ψ φ); trivial. lia.
  auto.
Qed.

Definition irreducible (Γ : env) :=
  (∀ p φ, (Var p → φ) ∈ Γ -> ¬ Var p ∈ Γ) /\
  ¬ ⊥ ∈ Γ /\
  ∀ φ ψ, ¬ (φ ∧ ψ) ∈ Γ /\ ¬ (φ ∨ ψ) ∈ Γ.

Definition make_conj x y := match x with
| ⊥ => ⊥
| (⊥→ ⊥) => y
| _ => match y with
    | ⊥ => ⊥
    | (⊥→ ⊥) => x
    | _ => if decide (x = y) then x else x ∧ y
    end
end.

Infix "⊼" := make_conj (at level 60).

Lemma make_conj_spec x y :
  {x = ⊥ ∧ x ⊼ y = ⊥} +
  {x = ⊤ ∧ x ⊼ y = y} +
  {y = ⊥ ∧ x ⊼ y = ⊥}+
  {y = ⊤ ∧ x ⊼ y = x} +
  {x = y ∧ x ⊼ y = x} +
  {x ⊼ y = (x ∧ y)}.
Proof.
unfold make_conj.
repeat (match goal with |- context [match ?x with | _ => _ end] => destruct x end; try tauto).
Qed.

Lemma occurs_in_make_conj v x y : occurs_in v (x ⊼ y) -> occurs_in v x \/ occurs_in v y.
Proof.
destruct (make_conj_spec x y) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm]; try tauto.
6:{ rewrite Hm. simpl. tauto. }
all:(destruct Hm as [Heq Hm]; rewrite Hm; simpl; tauto).
Qed.

Definition make_disj x y := match x with
| ⊥ => y
| (⊥→ ⊥) => (⊥→ ⊥)
| _ => match y with
    | ⊥ => x
    | (⊥→ ⊥) => (⊥→ ⊥)
    | _ => if decide (x = y) then x else x ∨ y
    end
end.

Infix "⊻" := make_disj (at level 65).

Lemma make_disj_spec x y :
  {x = ⊥ ∧ x ⊻ y = y} +
  {x = ⊤ ∧ x ⊻ y = ⊤} +
  {y = ⊥ ∧ x ⊻ y = x} +
  {y = ⊤ ∧ x ⊻ y = ⊤} +
  {x = y ∧ x ⊻ y = x} +
  {x ⊻ y = (x ∨ y)}.
Proof.
unfold make_disj.
repeat (match goal with |- context [match ?x with | _ => _ end] => destruct x end; try tauto).
Qed.

Lemma occurs_in_make_disj v x y : occurs_in v (x ⊻ y) -> occurs_in v x ∨ occurs_in v y.
Proof.
destruct (make_disj_spec x y) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm]; try tauto.
6:{ rewrite Hm. simpl. tauto. }
all:(destruct Hm as [Heq Hm]; rewrite Hm; simpl; tauto).
Qed.

(* "lazy" implication, which produces a potentially simpler, equivalent formula *)
Definition make_impl x y :=
match x with
| ⊥ => ⊤
| _ => match y with
  | ⊥ → ⊥ => ⊤
  | _ => x → y
  end
end.

Infix "⇢" := make_impl (at level 66).

Lemma make_impl_spec x y:
  {x = ⊥ ∧ x ⇢ y = ⊤} +
  {y = ⊤ ∧ x ⇢ y = ⊤} +
  {x ⇢ y = (x → y)}.
Proof.
unfold make_impl.
repeat (match goal with |- context [match ?x with | _ => _ end] => destruct x end; try tauto).
Qed.

Lemma occurs_in_make_impl v x y : occurs_in v (x ⇢ y) -> occurs_in v x ∨ occurs_in v y.
Proof.
destruct (make_impl_spec x y) as [[Hm|Hm]|Hm]; try tauto.
3:{ rewrite Hm. simpl. tauto. }
all:(destruct Hm as [Heq Hm]; rewrite Hm; simpl; tauto).
Qed.

Lemma occurs_in_make_impl2 v x y z: occurs_in v (x ⇢ (y ⇢ z)) -> occurs_in v x ∨ occurs_in v y ∨ occurs_in v z.
Proof.
intro H. apply occurs_in_make_impl in H. destruct H as [H|H]; try tauto.
apply occurs_in_make_impl in H. tauto.
Qed.

Definition conjunction l := foldl make_conj (⊥→ ⊥) (nodup form_eq_dec l).
Notation "⋀" := conjunction.

Definition disjunction l := foldl make_disj ⊥ (nodup form_eq_dec l).
Notation "⋁" := disjunction.

Lemma variables_conjunction x l : occurs_in x (⋀ l) -> exists φ, φ ∈ l /\ occurs_in x φ.
Proof.
unfold conjunction.
assert (Hcut : forall ψ, occurs_in x (foldl make_conj ψ (nodup form_eq_dec l))
  -> occurs_in x ψ \/ (∃ φ : form, (φ ∈ l ∧ occurs_in x φ)%type)).
{
induction l; simpl.
- tauto.
- intros ψ Hocc.
  case in_dec in Hocc; apply IHl in Hocc; simpl in Hocc;
  destruct Hocc as [Hx|(φ&Hin&Hx)]; try tauto.
  + right. exists φ. split; auto with *.
  + apply occurs_in_make_conj in Hx; destruct Hx as [Hx|Hx]; auto with *.
      right. exists a. auto with *.
  + right. exists φ. split; auto with *.
}
intro Hocc. apply Hcut in Hocc. simpl in Hocc. tauto.
Qed.

Lemma variables_disjunction x l : occurs_in x (⋁ l) -> exists φ, φ ∈ l /\ occurs_in x φ.
Proof.
unfold disjunction.
assert (Hcut : forall ψ, occurs_in x (foldl make_disj ψ (nodup form_eq_dec l))
  -> occurs_in x ψ \/ (∃ φ : form, (φ ∈ l ∧ occurs_in x φ)%type)).
{
induction l; simpl.
- tauto.
- intros ψ Hocc.
  case in_dec in Hocc; apply IHl in Hocc; simpl in Hocc;
  destruct Hocc as [Hx|(φ&Hin&Hx)]; try tauto.
  + right. exists φ. split; auto with *.
  + apply occurs_in_make_disj in Hx; destruct Hx as [Hx|Hx]; auto with *.
      right. exists a. auto with *.
  + right. exists φ. split; auto with *.
}
intro Hocc. apply Hcut in Hocc. simpl in Hocc. tauto.
Qed.

(* a dependent map on lists, with knowledge that we are on that list *)
(* should work with any set-like type *)

Program Fixpoint in_map_aux {A : Type} (Γ : env) (f : forall φ, (φ ∈ Γ) -> A)
 Γ' (HΓ' : Γ' ⊆ elements Γ) : list A:=
match Γ' with
| [] => []
| a::Γ' => f a _ :: in_map_aux Γ f Γ' _
end.
Next Obligation.
intros. apply gmultiset_elem_of_elements. auto with *.
Qed.
Next Obligation. auto with *. Qed.

Definition in_map {A : Type} (Γ : env)
  (f : forall φ, (φ ∈ Γ) -> A) : list A :=
  in_map_aux Γ f (elements Γ) (reflexivity _).

(* This generalises to any type. decidability of equality over this type is necessary for a result in "Type" *)
Lemma in_in_map {A : Type} {HD : forall a b : A, Decision (a = b)}
  Γ (f : forall φ, (φ ∈ Γ) -> A) ψ :
  ψ ∈ (in_map Γ f) -> {ψ0 & {Hin | ψ = f ψ0 Hin}}.
Proof.
unfold in_map.
assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ), ψ ∈ in_map_aux Γ f Γ' HΓ'
  → {ψ0 & {Hin : ψ0 ∈ Γ | ψ = f ψ0 Hin}}); [|apply Hcut].
induction Γ'; simpl; intros HΓ' Hin.
- contradict Hin. auto. now rewrite elem_of_nil.
- match goal with | H : ψ ∈ ?a :: (in_map_aux _ _ _ ?HΓ'') |- _ =>
  case (decide (ψ = a)); [| pose (myHΓ' := HΓ'')] end.
  + intro Heq; subst. exists a. eexists. reflexivity.
  + intro Hneq. apply (IHΓ' myHΓ').
    apply elem_of_cons in Hin. tauto.
Qed.

Local Definition in_subset {Γ : env} {Γ'} (Hi : Γ' ⊆ elements Γ) {ψ0} (Hin : ψ0 ∈ Γ') : ψ0 ∈ Γ.
Proof. apply gmultiset_elem_of_elements,Hi, Hin. Defined.

(* converse *)
(* we require proof irrelevance for the mapped function *)
Lemma in_map_in {A : Type} {HD : forall a b : A, Decision (a = b)}
  {Γ} {f : forall φ, (φ ∈ Γ) -> A} {ψ0} (Hin : ψ0 ∈ Γ):
  {Hin' | f ψ0 Hin' ∈ (in_map Γ f)}.
Proof.
unfold in_map.
assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ) ψ0 (Hin : In ψ0 Γ'),
  {Hin' | f ψ0 Hin' ∈ in_map_aux Γ f Γ' HΓ'}).
- induction Γ'; simpl; intros HΓ' ψ' Hin'; [auto with *|].
  case (decide (ψ' = a)).
  + intro; subst a. eexists. left.
  + intro Hneq. assert (Hin'' : In ψ' Γ') by (destruct Hin'; subst; tauto).
      pose (Hincl := (in_map_aux_obligation_2 Γ (a :: Γ') HΓ' a Γ' eq_refl)).
      destruct (IHΓ' Hincl ψ' Hin'') as [Hin0 Hprop].
      eexists. right. apply Hprop.
- destruct (Hcut (elements Γ) (reflexivity (elements Γ)) ψ0) as [Hin' Hprop].
  + now apply elem_of_list_In, gmultiset_elem_of_elements.
  + exists Hin'. exact Hprop.
Qed.

Lemma in_map_empty A f : @in_map A ∅ f = [].
Proof. auto with *. Qed.

Lemma in_map_ext {A} Δ f g:
  (forall φ H, f φ H = g φ H) -> @in_map A Δ f = in_map Δ g.
Proof.
  intros Heq.
  unfold in_map.
  assert(forall Γ HΓ, in_map_aux Δ f Γ HΓ = in_map_aux Δ g Γ HΓ); [|trivial].
  induction Γ; intro HΓ.
  - trivial.
  - simpl. now rewrite Heq, IHΓ.
Qed.

Global Instance env_order_trans : Transitive env_order.
Proof. unfold env_order. intros a b c H1 H2. now apply mord_trans with b. Qed.

Lemma env_order_singleton Δ φ : Δ ≺ Δ • φ.
Proof.
 unfold env_order. constructor.
 eapply MSetRed with (X := Δ ) (a := φ) (Y := ∅); try ms.
 intros y Hy. contradict Hy. apply gmultiset_not_elem_of_empty.
Qed.

Lemma env_order_singleton_compat {Δ Δ'} φ: (Δ ≺ Δ') -> (Δ • φ) ≺ (Δ' • φ).
Proof.
unfold env_order.
induction 1 as [Δ1 Δ2 [X a Y Heq1 Heq2 HY] |Δ1 Δ2 Δ3 Hlt1 Hlt Hind1 Hind2].
- constructor.
  eapply MSetRed with (X := X • φ) (a := a) (Y := Y).
  + rewrite Heq1. apply MSet.union_perm.
  + rewrite Heq2. apply MSet.union_perm.
  + assumption.
- econstructor 2; eauto.
Qed.

Lemma difference_singleton (Δ: env) (φ : form): φ ∈ Δ -> Δ ≡ ((Δ ∖ {[φ]}) • φ).
Proof.
intro Hin. rewrite (gmultiset_disj_union_difference {[φ]}) at 1. ms.
now apply gmultiset_singleton_subseteq_l.
Qed.

Lemma env_in_add (Δ : env) ϕ φ: φ ∈ (Δ • ϕ) <-> φ = ϕ \/ φ ∈ Δ.
Proof.
rewrite (gmultiset_elem_of_disj_union Δ), gmultiset_elem_of_singleton.
tauto.
Qed.

Lemma equiv_disj_union_compat_r {Δ Δ' Δ'' : env} : Δ ≡ Δ'' -> Δ ⊎ Δ' ≡ Δ'' ⊎ Δ'.
Proof. ms. Qed.

Lemma env_add_comm (Δ : env) φ ϕ : (Δ • φ • ϕ) ≡ (Δ • ϕ • φ).
Proof. ms. Qed.

Lemma in_difference (Δ : env) φ ψ : φ ≠ ψ -> φ ∈ Δ -> φ ∈ Δ ∖ {[ψ]}.
Proof.
intros Hne Hin.
unfold elem_of, gmultiset_elem_of.
rewrite (multiplicity_difference Δ {[ψ]} φ).
assert( HH := multiplicity_singleton_ne φ ψ Hne).
unfold singletonMS, base.singletonMS in HH.
unfold base.singleton, Environments.singleton. ms.
Qed.

Global Hint Resolve in_difference : multiset.

(* could be used in disj_inv *)
Lemma env_add_inv (Γ Γ' : env) (φ ψ : form): φ ≠ ψ -> ((Γ • φ) ≡ (Γ' • ψ)) -> (Γ' ≡ ((Γ ∖ {[ψ]}) • φ)).
Proof.
intros Hneq Heq.
rewrite <- env_replace; [rewrite Heq; ms|].
assert(ψ ∈ (Γ • φ)); [rewrite Heq|]; ms.
Qed.

Lemma env_add_inv' (Γ Γ' : env) (φ : form): (Γ • φ) ≡ Γ' -> (Γ ≡ (Γ' ∖ {[φ]})).
Proof. intro Heq. rewrite <- Heq. ms. Qed.

Lemma env_equiv_eq (Γ Γ' :env) : Γ = Γ' -> Γ ≡ Γ'.
Proof. intro; subst; trivial. Qed.

(* We need this induction principle in type. *)
Lemma gmultiset_rec (P : env → Type) :
  P ∅ → (∀ x X, P X → P ({[+ x +]} ⊎ X)) → ∀ X, P X.
Proof.
  intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
  destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
  rewrite (gmultiset_disj_union_difference' x X) by done.
  apply Hinsert, IH; multiset_solver.
Qed.

Section Order.

(* We introduce a notion of "pointed" environment, which is simply
 * a pair (Δ, φ), where Δ is an environment and φ is a formula,
 * not necessarily an element of Δ.  *)
Definition pointed_env := (env * form)%type.

(* The order on pointed environments is given by considering the
 * environment order on the sum of Δ and {φ}. *)
Definition pointed_env_order (pe1 : pointed_env) (pe2 : pointed_env) :=
  env_order (fst pe1 • snd pe1) (fst pe2 • snd pe2).

Lemma wf_pointed_order : well_founded pointed_env_order.
Proof.
  unfold pointed_env_order.
  apply Inverse_Image.wf_inverse_image, wf_env_order.
Qed.

End Order.

Infix "≺·" := pointed_env_order (at level 150).

Lemma difference_include (θ θ' : form) (Δ : env) :
  (θ' ∈ Δ) ->
  θ ∈ Δ ∖ {[θ']} -> θ ∈ Δ.
Proof.
intros Hin' Hin.
rewrite gmultiset_disj_union_difference with (X := {[θ']}).
- apply gmultiset_elem_of_disj_union. tauto.
- now apply gmultiset_singleton_subseteq_l.
Qed.

Lemma env_order_1 Δ φ1 φ : weight φ1 < weight φ -> Δ • φ1 ≺ Δ • φ.
Proof.
intros Hw.
constructor. econstructor; [reflexivity| reflexivity|].
intros y Hy. apply MSet.member_singleton in Hy. rewrite Hy. trivial.
Qed.

Global Instance assoc_meq_union : Assoc meq union.
Proof. intros x y z. ms. Qed.

Lemma env_order_2 Δ φ1 φ2 φ: weight φ1 < weight φ -> weight φ2 < weight φ -> Δ • φ1 • φ2 ≺ Δ • φ.
Proof.
intros Hw.
constructor. econstructor; [reflexivity| |].
- rewrite assoc; [reflexivity|]. apply assoc_meq_union.
- intros y Hy.
  apply MSet.member_union in Hy; destruct Hy as [Hy|Hy];
  apply MSet.member_singleton in Hy; now rewrite Hy.
Qed.

Lemma env_order_0 Δ φ: Δ ≺ Δ • φ.
Proof.
constructor. econstructor; [reflexivity| now rewrite MSet.union_empty|].
intros y Hy. exfalso. eapply MSet.not_empty; [exact Hy| ms].
Qed.

Lemma env_order_cancel_right Δ Δ' φ: (Δ ≺ Δ') -> Δ ≺ (Δ' • φ).
Proof. etransitivity; [|apply env_order_0]. assumption. Qed.

Lemma env_order_add_compat Δ Δ' φ : (Δ ≺ Δ') -> (Δ • φ) ≺ (Δ' • φ).
Proof.
  intro Hlt. induction Hlt as [Δ1 Δ2 Hlt | Δ1 Δ2 Δ0 Hlt1 IHHlt1 Hlt2 IHHlt2].
  - destruct Hlt as [Δ0 a Y Heq1 Heq2 Hall].
    constructor. apply (@MSetRed form_order _ _ (Δ0 • φ) a Y); ms.
  - unfold env_order. etransitivity; [exact IHHlt1| exact IHHlt2].
Qed.

Global Hint Resolve env_order_0 : order.
Global Hint Resolve env_order_1 : order.
Global Hint Resolve env_order_2 : order.
Global Hint Resolve env_order_add_compat : order.
Global Hint Resolve env_order_cancel_right : order.
Global Hint Extern 5 (?a < ?b) => subst; simpl; lia : order.

Lemma env_order_equiv_right_compat {Δ Δ' Δ'' : env}:
  Δ' ≡ Δ'' ->
  (Δ ≺ Δ'') ->
  Δ ≺ Δ'.
Proof. ms. Qed.

Ltac prepare_order := unfold pointed_env_order; subst; simpl; try match goal with
| Δ := _ |- _ => subst Δ; try prepare_order
| H : ?ψ ∈ ?Γ |- (?Γ ∖ {[?ψ]}) ≺ ?Γ => apply (env_order_equiv_right_compat (difference_singleton Γ ψ H))
| H : ?ψ ∈ ?Γ |- (?Γ ∖ {[?ψ]} • _) ≺ ?Γ =>
apply (env_order_equiv_right_compat (difference_singleton Γ ψ H))
| H : ?ψ ∈ ?Γ |- ((?Γ ∖ {[?ψ]} • _) • _) ≺ ?Γ =>
apply (env_order_equiv_right_compat (difference_singleton Γ ψ H))
| H : ?ψ ∈ ?Γ |- (?Γ ∖ {[?ψ]} • _ • _) ≺ ?Γ • ?φ =>
apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(difference_singleton Γ ψ H)))
| H : ?ψ ∈ ?Γ |- (?Γ ∖ {[?ψ]} • _ • _ • _) ≺ ?Γ • ?φ =>
apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(difference_singleton Γ ψ H)))
| H : ?ψ ∈ ?Γ |- (?Γ ∖ {[?ψ]} • _) ≺ ?Γ • ?φ =>
apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(difference_singleton Γ ψ H)))
end.

Global Hint Extern 2 ((?Γ ∖ {[?ψ]} , ?φ) ≺· (?Γ, ?φ)) => prepare_order : order.
Global Hint Extern 2 (?Γ ∖ {[?ψ]} • ?φ' • ?φ'' ≺ ?Γ • ?φ) => prepare_order : order.
Global Hint Extern 2 (?Γ ∖ {[?ψ]} • ?φ' ≺ ?Γ • ?φ) => prepare_order : order.

Lemma make_impl_weight φ ψ: weight (φ ⇢ ψ) <= weight (φ → ψ).
Proof.
destruct (make_impl_spec φ ψ) as [[[Heq' Heq]|[Heq' Heq]]|Heq]; subst; rewrite Heq; simpl.
- destruct ψ; simpl; lia.
- destruct φ; simpl; lia.
- trivial.
Qed.

Lemma make_impl_weight2 φ ψ θ: weight (φ ⇢ (ψ ⇢ θ)) <= weight (φ → (ψ → θ)).
Proof.
pose (make_impl_weight ψ θ).
pose (make_impl_weight φ (ψ ⇢ θ)).
simpl in *. lia.
Qed.

Global Hint Extern 5 (weight (?φ ⇢ ?ψ) < _) => (eapply le_lt_trans; [eapply make_impl_weight|]) : order.

Global Hint Extern 5 (weight (?φ ⇢ (?ψ ⇢ ?θ)) < _) => (eapply le_lt_trans; [eapply make_impl_weight2|]) : order.

Ltac order_tac := prepare_order; auto with order.

(* technical lemma : one can constructively find whether an environment contains
   an element satisfying a decidable property *)
Lemma decide_in (P : form -> Prop) (Γ : env) :
  (forall φ, Decision (P φ)) ->
  {φ : form| (φ ∈ Γ) /\ P φ} + {forall φ, φ ∈ Γ -> ¬ P φ}.
Proof.
intro HP.
induction Γ using gmultiset_rec.
- right. intros φ Hφ; inversion Hφ.
- destruct IHΓ as [(φ&Hφ) | HF].
  + left. exists φ. ms.
  + case (HP x); intro Hx.
    * left; exists x. ms.
    * right. intros. ms.
Qed.

Lemma union_difference_L (Γ : env) Δ ϕ: ϕ ∈ Γ -> (Γ ⊎ Δ) ∖ {[ϕ]} ≡ Γ ∖{[ϕ]} ⊎ Δ.
Proof. intro Hin. rewrite (difference_singleton _ _ Hin). ms. Qed.

Lemma union_difference_R (Γ : env) Δ ϕ: ϕ ∈ Δ -> (Γ ⊎ Δ) ∖ {[ϕ]} ≡ Γ ⊎ (Δ ∖{[ϕ]}).
Proof. intro Hin. rewrite (difference_singleton _ _ Hin). ms. Qed.

Global Instance equiv_assoc : @Assoc env equiv disj_union.
Proof. intros x y z. ms. Qed.
Global Hint Immediate equiv_assoc : proof.

Definition var_not_in_env p (Γ : env):= (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0).

(* helper tactic split cases given an assumption about belonging to a multiset *)

Ltac in_tac :=
repeat
match goal with
| H : ?θ ∈ {[?θ1; ?θ2]} |- _ => apply gmultiset_elem_of_union in H; destruct H as [H|H]; try subst
| H : ?θ ∈ (?Δ ∖ {[?θ']}) |- _ => apply difference_include in H; trivial
| H : context [?θ ∈ (?d • ?θ2)] |- _ =>
    rewrite (env_in_add d) in H; destruct H as [H|H]; try subst
| H : context [?θ ∈ {[ ?θ2 ]}] |- _ => rewrite gmultiset_elem_of_singleton in H; subst
end.

Ltac vars_tac :=
intros; subst;
repeat match goal with
| HE : context [occurs_in ?x (?E _ _)], H : occurs_in ?x (?E _ _) |- _ =>
    apply HE in H
end;
intuition;
repeat match goal with | H : exists x, _ |- _ => destruct H end;
intuition;
simpl in *; in_tac; try (split; [tauto || auto with *|]); simpl in *;
try match goal with
| H : occurs_in _ (?a ⇢ (?b ⇢ ?c)) |- _ => apply occurs_in_make_impl2 in H
| H : occurs_in _ (?a ⇢ ?b) |- _ => apply occurs_in_make_impl in H
end;
try multimatch goal with
| H : ?θ0 ∈ ?Δ0 |- context [exists θ, θ ∈ ?Δ /\ occurs_in ?x θ] =>
  solve[try right; exists θ0; split; [exact H|simpl; tauto]; eauto]
end.