KM.Sequent.Order
The weight of an environment
(* Note that a base 3 or 4 would suffice for IPC ; iSL requires 5 ;
but 9 allows admissibility proofs for KM to go through *)
Definition env_weight Γ :=
list_sum (map (fun x => 9 ^ weight x) Γ).
Lemma env_weight_disj_union Γ Δ :
env_weight (Γ ++ Δ) = env_weight Γ + env_weight Δ.
Proof.
unfold env_weight. now rewrite map_app, list_sum_app.
Qed.
Notation "Δ '•' φ" := (cons φ Δ) : list_scope.
Lemma env_weight_app Γ Δ :
env_weight (Γ ++ Δ) = env_weight Γ + env_weight Δ.
Proof.
unfold env_weight. now rewrite map_app,list_sum_app.
Qed.
Global Hint Rewrite env_weight_app : order.
Lemma env_weight_nil : env_weight [] = 0.
Proof. now unfold env_weight. Qed.
Global Hint Rewrite env_weight_nil : order.
Lemma env_weight_add Γ φ :
env_weight (Γ • φ) = env_weight Γ + (9 ^ weight φ).
Proof. unfold env_weight. simpl. lia. Qed.
Global Hint Rewrite env_weight_add : order.
Definition env_order := ltof _ env_weight.
Infix "≺" := env_order (at level 150).
Lemma env_weight_singleton (φ : form) :
env_weight [ φ ] = 9 ^ weight φ.
Proof.
unfold env_weight, ltof. simpl. lia.
Qed.
Lemma env_order_singleton φ ψ :
weight φ < weight ψ -> [φ ] ≺ [ ψ ].
Proof.
intro Hw. unfold env_order, ltof. do 2 rewrite env_weight_singleton.
apply Nat.pow_lt_mono_r. lia. trivial.
Qed.
Definition env_order_refl Δ Δ' := (env_weight Δ) ≤ (env_weight Δ').
Global Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150).
Lemma env_order_env_order_refl Δ Δ' :
env_order Δ Δ' -> env_order_refl Δ Δ'.
Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
Global Hint Resolve env_order_env_order_refl: order.
Lemma env_order_self Δ : Δ ≼ Δ.
Proof. unfold env_order_refl. trivial. Qed.
Global Instance Proper_env_weight : Proper ((≡ₚ) ==> (=)) env_weight.
Proof.
intros Γ Δ Heq. unfold env_weight. now rewrite Heq.
Qed.
Global Instance Proper_env_order_refl_env_weight:
Proper ((env_order_refl) ==> le) env_weight.
Proof. intros Γ Δ Hle. auto with *. Qed.
Global Hint Resolve Proper_env_order_refl_env_weight : order.
Global Hint Unfold form_order : mset.
Global Instance env_order_trans : Transitive env_order.
Proof. unfold env_order, env_weight, ltof. auto with *. Qed.
Definition wf_env_order : well_founded env_order.
Proof. now apply well_founded_lt_compat with env_weight.
Defined.
(* 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 env_pair := (list form * list form)%type.
(* The order on sequents (Γ ⇒ Δ) is given by considering the
* environment order on the sum of Γ and two copies of Δ. *)
Definition env_pair_order (pe1 : env_pair) (pe2 : env_pair) :=
env_order (fst pe1 ++ snd pe1 ++ snd pe1) (fst pe2 ++ snd pe2 ++ snd pe2).
Lemma wf_pointed_order : well_founded env_pair_order.
Proof. apply well_founded_ltof. Qed.
Definition env_pair_ms_order (Γφ Δψ : env * env) :=
env_pair_order (elements Γφ.1, elements Γφ.2) (elements Δψ.1, elements Δψ.2).
Lemma wf_env_pair_ms_order : well_founded env_pair_ms_order.
Proof. apply well_founded_ltof. Qed.
Infix "≺·" := env_pair_order (at level 150).
Lemma env_order_equiv_right_compat {Δ Δ' Δ'' }:
Δ' ≡ₚ Δ'' ->
(Δ ≺ Δ'') ->
Δ ≺ Δ'.
Proof.
unfold equiv, env_order, ltof, env_weight. intro Heq. rewrite Heq. trivial.
Qed.
Lemma env_order_equiv_left_compat {Δ Δ' Δ'' }:
Δ ≡ₚ Δ'' ->
(Δ'' ≺ Δ') ->
Δ ≺ Δ'.
Proof. unfold equiv, env_order, ltof, env_weight. intro Heq. rewrite Heq. trivial. Qed.
Global Instance Proper_env_order:
Proper ((≡ₚ) ==> (≡ₚ) ==> (fun x y => x <-> y)) env_order.
Proof.
intros Δ1 Δ2 H12 Δ3 Δ4 H34; unfold equiv, env_order, ltof, env_weight.
rewrite H12, H34. tauto.
Qed.
Global Instance Proper_env_order_refl:
Proper ((≡ₚ) ==> (≡ₚ) ==> (fun x y => x <-> y)) env_order_refl.
Proof.
intros Δ1 Δ2 H12 Δ3 Δ4 H34; unfold equiv, env_order, ltof, env_weight, env_order_refl.
now rewrite H12, H34.
Qed.
Local Hint Resolve Nat.pow_lt_mono_r : order.
Lemma env_order_compat Δ Δ' φ1 φ :
weight φ1 < weight φ -> (Δ' ≼ Δ) -> Δ' • φ1 ≺ Δ • φ.
Proof.
intros. unfold env_order, ltof. repeat rewrite env_weight_add.
apply Nat.add_le_lt_mono; auto with *.
Qed.
Global Hint Resolve env_order_compat : order.
Lemma env_order_compat' Δ Δ' φ1 φ :
weight φ1 ≤ weight φ -> (Δ' ≺ Δ ) -> Δ' • φ1 ≺ Δ • φ.
Proof.
intros. unfold env_order, ltof. repeat rewrite env_weight_add.
apply Nat.add_lt_le_mono; auto with *. now apply Nat.pow_le_mono_r.
Qed.
Global Hint Resolve env_order_compat' : order.
Lemma env_order_add_compat Δ Δ' φ : (Δ ≺ Δ') -> (Δ • φ) ≺ (Δ' • φ).
Proof.
unfold env_order, ltof. do 2 rewrite env_weight_add. lia.
Qed.
Lemma env_order_disj_union_compat_left Δ Δ' Δ'':
(Δ ≺ Δ'') -> Δ ++ Δ' ≺ Δ'' ++ Δ'.
Proof.
unfold env_order, ltof. intro. do 2 rewrite env_weight_disj_union. lia.
Qed.
Lemma env_order_disj_union_compat_right Δ Δ' Δ'':
(Δ ≺ Δ'') -> Δ' ++ Δ ≺ Δ' ++ Δ''.
Proof.
unfold env_order, ltof. repeat rewrite env_weight_disj_union. lia.
Qed.
Global Hint Resolve env_order_disj_union_compat_right : order.
Lemma env_order_disj_union_compat Δ Δ' Δ'' Δ''':
(Δ ≺ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
Proof.
unfold env_order, ltof. repeat rewrite env_weight_disj_union. lia.
Qed.
Lemma env_order_refl_disj_union_compat Δ Δ' Δ'' Δ''':
(env_order_refl Δ Δ'') -> (env_order_refl Δ' Δ''') -> env_order_refl (Δ ++ Δ') (Δ'' ++ Δ''').
Proof.
unfold env_order_refl, env_order, ltof. repeat rewrite env_weight_disj_union.
intros Hle1 Hle2; try rewrite Heq1; try rewrite Heq2; try lia.
Qed.
Global Hint Resolve env_order_refl_disj_union_compat : order.
Hint Unfold env_order_refl : order.
Lemma env_order_disj_union_compat_strong_right Δ Δ' Δ'' Δ''':
(Δ ≺ Δ'') -> (Δ' ≼ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
Proof.
intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia.
Qed.
Lemma env_order_disj_union_compat_strong_left Δ Δ' Δ'' Δ''':
(Δ ≼ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
Proof.
intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. Qed.
Global Hint Resolve env_order_disj_union_compat_strong_left : order.
Global Hint Resolve elements_open_boxes : order.
Lemma weight_open_box φ : weight (⊙ φ) ≤ weight φ.
Proof. dependent destruction φ; simpl; lia. Qed.
Lemma open_boxes_env_order Δ : (map open_box Δ) ≼ Δ.
Proof.
unfold env_order_refl.
induction Δ as [|φ Δ]; trivial.
simpl. do 2 rewrite env_weight_add. dependent destruction φ; simpl; lia.
Qed.
Global Hint Resolve open_boxes_env_order : order.
Local Lemma pow9_gt_0 n : 1 ≤ 9 ^ n.
Proof. transitivity (9^0). simpl. lia. apply Nat.pow_le_mono_r; lia. Qed.
Local Hint Resolve pow9_gt_0: order.
Lemma env_order_0 Δ Δ' φ: (Δ' ≼ Δ) -> Δ' ≺ Δ • φ.
Proof.
intros Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
unfold env_order_refl in Hor.
pose (pow9_gt_0 ((weight φ))).
lia.
Qed.
Lemma env_order_1 Δ Δ' φ1 φ : weight φ1 < weight φ -> (Δ' ≼ Δ) -> Δ' • φ1 ≺ Δ • φ.
Proof.
intros Hw1 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
repeat (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
lia.
Qed.
Lemma env_order_2 Δ Δ' φ1 φ2 φ: weight φ1 < weight φ -> weight φ2 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
repeat (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
lia.
Qed.
Lemma env_order_3 Δ Δ' φ1 φ2 φ3 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ -> (Δ' ≼ Δ) ->
Δ' • φ1 • φ2 • φ3 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 3 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
lia.
Qed.
Lemma env_order_4 Δ Δ' φ1 φ2 φ3 φ4 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ -> weight φ4 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 4 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_5 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 5 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_6 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ6 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ -> weight φ6 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 • φ6 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hw6 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 6 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_7 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ6 φ7 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ -> weight φ6 < weight φ ->
weight φ7 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 • φ6 • φ7 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hw6 Hw7 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 7 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_8 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ6 φ7 φ8 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ -> weight φ6 < weight φ ->
weight φ7 < weight φ -> weight φ8 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 • φ6 • φ7 • φ8 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hw6 Hw7 Hw8 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 8 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_cancel_singleton_right Δ Δ' φ: (Δ ≺ Δ') -> Δ ≺ (Δ' • φ).
Proof. etransitivity; [|apply env_order_0]; eauto. left. Qed.
Lemma env_order_cancel_left Δ Δ' Δ'': (Δ ≺ Δ') -> Δ ≺ (Δ'' ++ Δ').
Proof.
intro Hlt. induction Δ''; trivial.
rewrite Permutation_cons_append, app_Permutation_comm.
rewrite <- Permutation_cons_append, <- Permutation_middle.
apply env_order_cancel_singleton_right.
now rewrite app_Permutation_comm.
Qed.
Lemma env_order_cancel_right Δ Δ' Δ'': (Δ ≺ Δ'') -> Δ ≺ (Δ'' ++ Δ').
Proof. rewrite Permutation_app_comm. apply env_order_cancel_left. Qed.
Lemma env_order_refl_cancel_right Δ Δ' Δ'': (env_order_refl Δ Δ'') -> env_order_refl Δ (Δ'' ++ Δ').
Proof. unfold env_order_refl. simpl. rewrite env_weight_app. lia. Qed.
Lemma env_order_refl_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ).
Proof. unfold env_order_refl. do 2 rewrite env_weight_add. lia. Qed.
Lemma env_order_refl_add' Δ Δ' φ φ': weight φ ≤ weight φ' -> (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ').
Proof. unfold env_order_refl. do 2 rewrite env_weight_add.
intros. apply Nat.add_le_mono. lia. apply Nat.pow_le_mono_r; lia. Qed.
Global Hint Resolve env_order_disj_union_compat_left : order.
Global Hint Resolve env_order_disj_union_compat_right : order.
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_3 : order.
Global Hint Resolve env_order_4 : order.
Global Hint Resolve env_order_5 : order.
Global Hint Resolve env_order_6 : order.
Global Hint Resolve env_order_7 : order.
Global Hint Resolve env_order_8 : order.
Global Hint Resolve env_order_add_compat : order.
Global Hint Resolve env_order_cancel_right : order.
Global Hint Resolve env_order_refl_cancel_right : order.
Global Hint Resolve env_order_cancel_left : order.
Global Hint Resolve env_order_refl_add : order.
Global Hint Resolve env_order_refl_add' : order.
Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order.
Ltac get_diff_form g := match g with
| ?Γ ∖{[?φ]} => φ
| _ (?Γ ∖{[?φ]}) => φ
| _ (rm ?φ _) => φ
| (rm ?φ _) => φ
| ?Γ ++ _ => get_diff_form Γ
| _ :: ?Γ => get_diff_form Γ
end.
Ltac get_diff_env g := match g with
| ?Γ ∖{[?φ]} => Γ
| _ :: ?Γ => get_diff_env Γ
end.
Lemma remove_env_order Δ φ: rm φ Δ ≼ Δ.
Proof.
unfold env_order_refl.
induction Δ as [|ψ Δ]. trivial.
simpl. destruct form_eq_dec; repeat rewrite env_weight_add; lia.
Qed.
Global Hint Resolve remove_env_order : order.
Lemma remove_In_env_order_refl Δ φ: In φ Δ -> rm φ Δ • φ ≼ Δ.
Proof.
induction Δ as [|ψ Δ].
- intro Hf; contradict Hf.
- intros [Heq | Hin].
+ subst. simpl. destruct form_eq_dec; [|tauto]. auto with order.
+ specialize (IHΔ Hin). simpl. case form_eq_dec as [Heq | Hneq].
* subst. auto with order.
* rewrite (Permutation_swap ψ φ (rm φ Δ)). auto with order.
Qed.
Global Hint Resolve remove_In_env_order_refl : order.
Lemma Permutation_rm φ Γ : φ ∈ Γ -> Γ ≡ₚ φ :: rm φ Γ.
Proof.
induction Γ as [| a Γ]; intro Hin.
- inversion Hin.
- simpl. case (form_eq_dec φ a).
+ intro; subst; trivial.
+ intro. rewrite Permutation_swap. auto with *.
Qed.
Lemma env_order_lt_le_trans Γ Γ' Γ'' : (Γ ≺ Γ') -> (Γ' ≼ Γ'') -> Γ ≺ Γ''.
Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
Lemma env_order_le_lt_trans Γ Γ' Γ'' : (Γ ≼ Γ') -> (Γ' ≺ Γ'') -> Γ ≺ Γ''.
Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
Lemma remove_In_env_order Δ φ: In φ Δ -> rm φ Δ ≺ Δ.
Proof.
intro Hin. apply remove_In_env_order_refl in Hin.
eapply env_order_lt_le_trans; [|apply Hin]. auto with order.
Qed.
Global Hint Resolve remove_In_env_order : order.
Lemma elem_of_list_In_1 {A : Type}: ∀ (l : list A) (x : A), x ∈ l <-> In x l.
Proof. apply elem_of_list_In. Qed.
Global Hint Resolve elem_of_list_In_1 : order.
Lemma elements_elem_of {Γ : env} {φ : form} :
φ ∈ Γ -> elements Γ ≡ₚ φ :: elements (Γ ∖ {[φ]}).
Proof.
intro Hin. setoid_rewrite <- elements_env_add.
apply Proper_elements, symmetry, difference_singleton, Hin.
Qed.
Lemma env_pair_order_cancel_right p Γ Δ Δ' : (p ≺· (Γ, Δ)) -> (p ≺· (Γ, Δ ++ Δ')).
Proof.
unfold env_pair_order. simpl. intro.
repeat rewrite app_assoc. apply env_order_cancel_right.
repeat rewrite <- app_assoc. rewrite (Permutation_app_comm Δ' Δ).
repeat rewrite app_assoc.
apply env_order_cancel_right.
repeat rewrite <- app_assoc. trivial.
Qed.
Lemma env_pair_order_cancel_left p Γ Δ Δ' : (p ≺· (Γ, Δ')) -> (p ≺· (Γ, Δ ++ Δ')).
Proof.
unfold env_pair_order. simpl. intro. rewrite (Permutation_app_comm Δ Δ').
apply env_pair_order_cancel_right, H.
Qed.
Ltac prepare_order :=
repeat (apply env_order_add_compat);
unfold env_pair_order; subst; simpl; repeat rewrite open_boxes_add; try multimatch goal with
| Δ := _ |- _ => subst Δ; try prepare_order
| Hin : ?a ∈ ?Γ |- context[elements ?Γ] => rewrite (elements_elem_of Hin); try prepare_order
| Hin' : ?b ∈ ?Γ, Hin : ?a ∈ ?Γ |- context[?Γ ++ ?Δ] => rewrite (Permutation_app_tail Δ (Permutation_rm _ _ Hin')); try prepare_order
| Hin : ?a ∈ ?Γ |- context[?Γ ++ ?Δ] => rewrite (Permutation_app_tail Δ (Permutation_rm _ _ Hin)); try prepare_order
| Hin : ?a ∈ ?Δ |- context[?Γ ++ ?Δ] => rewrite (Permutation_app_head Γ (Permutation_rm _ _ Hin)); try prepare_order
| H : _ ∈ list_to_set_disj _ |- _ => apply elem_of_list_to_set_disj in H; try prepare_order
| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ => let ψ' := (get_diff_form Γ') in
apply (env_order_equiv_right_compat (difference_singleton Γ ψ' H)) ||
(eapply env_order_lt_le_trans ; [| apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial])
| H : ?ψ ∈ ?Γ |- ?Γ' ≺ (?φ :: ?Γ) => let ψ' := (get_diff_form Γ') in
apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))
| H : ?ψ ∈ ?Γ |- ?Γ' ≺ (_ :: _ :: ?Γ) => let ψ' := (get_diff_form Γ') in
apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))) ||
(eapply env_order_le_lt_trans; [| apply env_order_add_compat;
eapply env_order_lt_le_trans; [| (apply env_order_refl_add; apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial) ] ] )
|H : ?a = _ |- context[?a] => rewrite H; try prepare_order
end.
Lemma openboxes_env_order Δ δ : (map open_box Δ) • δ • δ ≺ Δ • □ δ.
Proof.
induction Δ as [|x Δ].
- simpl. unfold env_order, ltof, env_weight. simpl.
repeat rewrite <- plus_n_O. apply Nat.add_lt_mono_l.
rewrite plus_n_O at 1. auto with *.
- apply (env_order_equiv_right_compat (Δ'' := Δ • □ δ • x)); [constructor|].
simpl.
eapply (env_order_equiv_left_compat (Δ'' := map open_box Δ • δ • δ • ⊙ x)).
+ do 2 (rewrite (Permutation_swap δ (⊙ x)); apply Permutation_skip). trivial.
+ dependent destruction x; intros; simpl; try (solve[now apply env_order_add_compat]).
transitivity (x :: (□δ) :: Δ).
* auto with *.
* apply env_order_1; simpl; auto. left.
Qed.
Lemma env_order_open_box Γ φ (Hin : (□ φ) ∈ Γ) : □⁻¹ Γ ≺ Γ.
Proof.
induction Γ as [|x Γ] ; cbn ; [ inversion Hin | ].
inversion Hin ; subst.
- cbn. apply env_order_1 ; cbn ; [ lia | apply open_boxes_env_order ].
- destruct x ; cbn ; try ( now apply env_order_add_compat ; auto).
apply env_order_1 ; [ cbn ; lia | apply env_order_env_order_refl ; auto].
Qed.
Global Hint Resolve env_order_open_box : order.
Global Hint Resolve openboxes_env_order : order.
Lemma weight_Arrow_1 φ ψ : 1 < weight (φ → ψ).
Proof. simpl. pose (weight_pos φ). lia. Qed.
Lemma weight_Box_1 φ: 1 < weight (□ φ).
Proof. simpl. pose (weight_pos φ). lia. Qed.
Global Hint Resolve weight_Arrow_1 : order.
Global Hint Resolve weight_Box_1 : order.
Lemma env_order_empty Δ : (elements (∅ : env)) ≼ Δ.
Proof.
unfold env_order_refl. setoid_rewrite gmultiset_elements_empty.
unfold env_weight. simpl. lia.
Qed.
Global Hint Resolve env_order_empty : order.
Ltac order_tac :=
try unfold env_pair_ms_order; prepare_order;
try replace (elements ∅) with ([] : list form) by ms;
repeat rewrite elements_open_boxes;
repeat rewrite env_replace by ms;
repeat rewrite env_add_remove;
repeat rewrite elements_env_add;
repeat rewrite Permutation_middle;
simpl; auto 10 with order;
repeat (apply env_order_disj_union_compat_right; order_tac).
Global Hint Extern 5 (?a ≺ ?b) => order_tac : proof.
Hint Extern 5 (?a ≺· ?b) => order_tac : proof.
Lemma env_pair_order_bot_R pe Δ Δ': (pe ≺· (Δ, [])) -> pe ≺· (Δ, Δ').
Proof.
intro Hlt. destruct pe as (Γ, ψ). unfold env_pair_order. simpl.
eapply env_order_lt_le_trans. exact Hlt. simpl.
unfold env_order_refl. repeat rewrite env_weight_add.
simpl. repeat rewrite env_weight_app, ?env_weight_nil. lia.
Qed.
Hint Resolve env_pair_order_bot_R : order.
Lemma env_pair_order_bot_L pe Δ φ: ((Δ, φ) ≺· pe) -> (Δ, []) ≺· pe.
Proof.
intro Hlt. destruct pe as (Γ, ψ). unfold env_pair_order. simpl.
eapply env_order_le_lt_trans; [|exact Hlt]. simpl.
unfold env_order_refl. repeat rewrite ?env_weight_app, ?env_weight_nil. lia.
Qed.
Lemma env_pair_order_botf_L pe Δ φ: ((Δ, φ) ≺· pe) -> (Δ, []) ≺· pe.
Proof.
intro Hlt. destruct pe as (Γ, ψ). unfold env_pair_order. simpl.
eapply env_order_le_lt_trans; [|exact Hlt]. simpl.
unfold env_order_refl. repeat rewrite ?env_weight_app, ?env_weight_nil. lia.
Qed.
Hint Resolve env_pair_order_bot_L : order.
Lemma weight_or_bot a b: weight(⊥) < weight (a ∨b).
Proof. destruct a; simpl; lia. Qed.
Hint Resolve weight_or_bot : order.
Definition env_pair_order_refl (pe1 : env_pair) (pe2 : env_pair) :=
env_order_refl (fst pe1 ++ snd pe1 ++ snd pe1) (fst pe2 ++ snd pe2 ++ snd pe2).
Lemma env_pair_order_l (Γ Γ' Δ : list form) : (Γ ≺ Γ') -> (Γ, Δ) ≺· (Γ', Δ).
Proof.
intro. unfold env_pair_order. simpl. now apply env_order_disj_union_compat_left.
Qed.
Hint Resolve env_pair_order_l : order.
Lemma env_pair_order_nil_l (Γ Γ' Δ : list form) : (Γ ≺ Γ') -> (Γ, []) ≺· (Γ', Δ).
Proof. unfold env_pair_order, env_order, ltof. simpl.
repeat rewrite env_weight_app, ?env_weight_nil. lia.
Qed.
Hint Resolve env_pair_order_nil_l : order.
but 9 allows admissibility proofs for KM to go through *)
Definition env_weight Γ :=
list_sum (map (fun x => 9 ^ weight x) Γ).
Lemma env_weight_disj_union Γ Δ :
env_weight (Γ ++ Δ) = env_weight Γ + env_weight Δ.
Proof.
unfold env_weight. now rewrite map_app, list_sum_app.
Qed.
Notation "Δ '•' φ" := (cons φ Δ) : list_scope.
Lemma env_weight_app Γ Δ :
env_weight (Γ ++ Δ) = env_weight Γ + env_weight Δ.
Proof.
unfold env_weight. now rewrite map_app,list_sum_app.
Qed.
Global Hint Rewrite env_weight_app : order.
Lemma env_weight_nil : env_weight [] = 0.
Proof. now unfold env_weight. Qed.
Global Hint Rewrite env_weight_nil : order.
Lemma env_weight_add Γ φ :
env_weight (Γ • φ) = env_weight Γ + (9 ^ weight φ).
Proof. unfold env_weight. simpl. lia. Qed.
Global Hint Rewrite env_weight_add : order.
Definition env_order := ltof _ env_weight.
Infix "≺" := env_order (at level 150).
Lemma env_weight_singleton (φ : form) :
env_weight [ φ ] = 9 ^ weight φ.
Proof.
unfold env_weight, ltof. simpl. lia.
Qed.
Lemma env_order_singleton φ ψ :
weight φ < weight ψ -> [φ ] ≺ [ ψ ].
Proof.
intro Hw. unfold env_order, ltof. do 2 rewrite env_weight_singleton.
apply Nat.pow_lt_mono_r. lia. trivial.
Qed.
Definition env_order_refl Δ Δ' := (env_weight Δ) ≤ (env_weight Δ').
Global Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150).
Lemma env_order_env_order_refl Δ Δ' :
env_order Δ Δ' -> env_order_refl Δ Δ'.
Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
Global Hint Resolve env_order_env_order_refl: order.
Lemma env_order_self Δ : Δ ≼ Δ.
Proof. unfold env_order_refl. trivial. Qed.
Global Instance Proper_env_weight : Proper ((≡ₚ) ==> (=)) env_weight.
Proof.
intros Γ Δ Heq. unfold env_weight. now rewrite Heq.
Qed.
Global Instance Proper_env_order_refl_env_weight:
Proper ((env_order_refl) ==> le) env_weight.
Proof. intros Γ Δ Hle. auto with *. Qed.
Global Hint Resolve Proper_env_order_refl_env_weight : order.
Global Hint Unfold form_order : mset.
Global Instance env_order_trans : Transitive env_order.
Proof. unfold env_order, env_weight, ltof. auto with *. Qed.
Definition wf_env_order : well_founded env_order.
Proof. now apply well_founded_lt_compat with env_weight.
Defined.
(* 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 env_pair := (list form * list form)%type.
(* The order on sequents (Γ ⇒ Δ) is given by considering the
* environment order on the sum of Γ and two copies of Δ. *)
Definition env_pair_order (pe1 : env_pair) (pe2 : env_pair) :=
env_order (fst pe1 ++ snd pe1 ++ snd pe1) (fst pe2 ++ snd pe2 ++ snd pe2).
Lemma wf_pointed_order : well_founded env_pair_order.
Proof. apply well_founded_ltof. Qed.
Definition env_pair_ms_order (Γφ Δψ : env * env) :=
env_pair_order (elements Γφ.1, elements Γφ.2) (elements Δψ.1, elements Δψ.2).
Lemma wf_env_pair_ms_order : well_founded env_pair_ms_order.
Proof. apply well_founded_ltof. Qed.
Infix "≺·" := env_pair_order (at level 150).
Lemma env_order_equiv_right_compat {Δ Δ' Δ'' }:
Δ' ≡ₚ Δ'' ->
(Δ ≺ Δ'') ->
Δ ≺ Δ'.
Proof.
unfold equiv, env_order, ltof, env_weight. intro Heq. rewrite Heq. trivial.
Qed.
Lemma env_order_equiv_left_compat {Δ Δ' Δ'' }:
Δ ≡ₚ Δ'' ->
(Δ'' ≺ Δ') ->
Δ ≺ Δ'.
Proof. unfold equiv, env_order, ltof, env_weight. intro Heq. rewrite Heq. trivial. Qed.
Global Instance Proper_env_order:
Proper ((≡ₚ) ==> (≡ₚ) ==> (fun x y => x <-> y)) env_order.
Proof.
intros Δ1 Δ2 H12 Δ3 Δ4 H34; unfold equiv, env_order, ltof, env_weight.
rewrite H12, H34. tauto.
Qed.
Global Instance Proper_env_order_refl:
Proper ((≡ₚ) ==> (≡ₚ) ==> (fun x y => x <-> y)) env_order_refl.
Proof.
intros Δ1 Δ2 H12 Δ3 Δ4 H34; unfold equiv, env_order, ltof, env_weight, env_order_refl.
now rewrite H12, H34.
Qed.
Local Hint Resolve Nat.pow_lt_mono_r : order.
Lemma env_order_compat Δ Δ' φ1 φ :
weight φ1 < weight φ -> (Δ' ≼ Δ) -> Δ' • φ1 ≺ Δ • φ.
Proof.
intros. unfold env_order, ltof. repeat rewrite env_weight_add.
apply Nat.add_le_lt_mono; auto with *.
Qed.
Global Hint Resolve env_order_compat : order.
Lemma env_order_compat' Δ Δ' φ1 φ :
weight φ1 ≤ weight φ -> (Δ' ≺ Δ ) -> Δ' • φ1 ≺ Δ • φ.
Proof.
intros. unfold env_order, ltof. repeat rewrite env_weight_add.
apply Nat.add_lt_le_mono; auto with *. now apply Nat.pow_le_mono_r.
Qed.
Global Hint Resolve env_order_compat' : order.
Lemma env_order_add_compat Δ Δ' φ : (Δ ≺ Δ') -> (Δ • φ) ≺ (Δ' • φ).
Proof.
unfold env_order, ltof. do 2 rewrite env_weight_add. lia.
Qed.
Lemma env_order_disj_union_compat_left Δ Δ' Δ'':
(Δ ≺ Δ'') -> Δ ++ Δ' ≺ Δ'' ++ Δ'.
Proof.
unfold env_order, ltof. intro. do 2 rewrite env_weight_disj_union. lia.
Qed.
Lemma env_order_disj_union_compat_right Δ Δ' Δ'':
(Δ ≺ Δ'') -> Δ' ++ Δ ≺ Δ' ++ Δ''.
Proof.
unfold env_order, ltof. repeat rewrite env_weight_disj_union. lia.
Qed.
Global Hint Resolve env_order_disj_union_compat_right : order.
Lemma env_order_disj_union_compat Δ Δ' Δ'' Δ''':
(Δ ≺ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
Proof.
unfold env_order, ltof. repeat rewrite env_weight_disj_union. lia.
Qed.
Lemma env_order_refl_disj_union_compat Δ Δ' Δ'' Δ''':
(env_order_refl Δ Δ'') -> (env_order_refl Δ' Δ''') -> env_order_refl (Δ ++ Δ') (Δ'' ++ Δ''').
Proof.
unfold env_order_refl, env_order, ltof. repeat rewrite env_weight_disj_union.
intros Hle1 Hle2; try rewrite Heq1; try rewrite Heq2; try lia.
Qed.
Global Hint Resolve env_order_refl_disj_union_compat : order.
Hint Unfold env_order_refl : order.
Lemma env_order_disj_union_compat_strong_right Δ Δ' Δ'' Δ''':
(Δ ≺ Δ'') -> (Δ' ≼ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
Proof.
intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia.
Qed.
Lemma env_order_disj_union_compat_strong_left Δ Δ' Δ'' Δ''':
(Δ ≼ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
Proof.
intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. Qed.
Global Hint Resolve env_order_disj_union_compat_strong_left : order.
Global Hint Resolve elements_open_boxes : order.
Lemma weight_open_box φ : weight (⊙ φ) ≤ weight φ.
Proof. dependent destruction φ; simpl; lia. Qed.
Lemma open_boxes_env_order Δ : (map open_box Δ) ≼ Δ.
Proof.
unfold env_order_refl.
induction Δ as [|φ Δ]; trivial.
simpl. do 2 rewrite env_weight_add. dependent destruction φ; simpl; lia.
Qed.
Global Hint Resolve open_boxes_env_order : order.
Local Lemma pow9_gt_0 n : 1 ≤ 9 ^ n.
Proof. transitivity (9^0). simpl. lia. apply Nat.pow_le_mono_r; lia. Qed.
Local Hint Resolve pow9_gt_0: order.
Lemma env_order_0 Δ Δ' φ: (Δ' ≼ Δ) -> Δ' ≺ Δ • φ.
Proof.
intros Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
unfold env_order_refl in Hor.
pose (pow9_gt_0 ((weight φ))).
lia.
Qed.
Lemma env_order_1 Δ Δ' φ1 φ : weight φ1 < weight φ -> (Δ' ≼ Δ) -> Δ' • φ1 ≺ Δ • φ.
Proof.
intros Hw1 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
repeat (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
lia.
Qed.
Lemma env_order_2 Δ Δ' φ1 φ2 φ: weight φ1 < weight φ -> weight φ2 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
repeat (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
lia.
Qed.
Lemma env_order_3 Δ Δ' φ1 φ2 φ3 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ -> (Δ' ≼ Δ) ->
Δ' • φ1 • φ2 • φ3 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 3 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
lia.
Qed.
Lemma env_order_4 Δ Δ' φ1 φ2 φ3 φ4 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ -> weight φ4 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 4 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_5 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 5 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_6 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ6 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ -> weight φ6 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 • φ6 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hw6 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 6 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_7 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ6 φ7 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ -> weight φ6 < weight φ ->
weight φ7 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 • φ6 • φ7 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hw6 Hw7 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 7 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_8 Δ Δ' φ1 φ2 φ3 φ4 φ5 φ6 φ7 φ8 φ:
weight φ1 < weight φ -> weight φ2 < weight φ -> weight φ3 < weight φ ->
weight φ4 < weight φ -> weight φ5 < weight φ -> weight φ6 < weight φ ->
weight φ7 < weight φ -> weight φ8 < weight φ ->
(Δ' ≼ Δ) -> Δ' • φ1 • φ2 • φ3 • φ4 • φ5 • φ6 • φ7 • φ8 ≺ Δ • φ.
Proof.
intros Hw1 Hw2 Hw3 Hw4 Hw5 Hw6 Hw7 Hw8 Hor.
unfold env_order, ltof. repeat rewrite env_weight_add.
apply Proper_env_order_refl_env_weight in Hor.
replace (weight φ) with (S (pred (weight φ))) by lia.
apply Nat.lt_le_pred in Hw1, Hw2.
simpl. repeat rewrite Nat.add_assoc.
pose (pow9_gt_0 (Init.Nat.pred (weight φ))).
rewrite Nat.add_0_r.
do 8 (apply Nat.add_lt_le_mono; [|apply Nat.pow_le_mono_r; lia]).
pose (pow9_gt_0 (Init.Nat.pred (weight φ))). lia.
Qed.
Lemma env_order_cancel_singleton_right Δ Δ' φ: (Δ ≺ Δ') -> Δ ≺ (Δ' • φ).
Proof. etransitivity; [|apply env_order_0]; eauto. left. Qed.
Lemma env_order_cancel_left Δ Δ' Δ'': (Δ ≺ Δ') -> Δ ≺ (Δ'' ++ Δ').
Proof.
intro Hlt. induction Δ''; trivial.
rewrite Permutation_cons_append, app_Permutation_comm.
rewrite <- Permutation_cons_append, <- Permutation_middle.
apply env_order_cancel_singleton_right.
now rewrite app_Permutation_comm.
Qed.
Lemma env_order_cancel_right Δ Δ' Δ'': (Δ ≺ Δ'') -> Δ ≺ (Δ'' ++ Δ').
Proof. rewrite Permutation_app_comm. apply env_order_cancel_left. Qed.
Lemma env_order_refl_cancel_right Δ Δ' Δ'': (env_order_refl Δ Δ'') -> env_order_refl Δ (Δ'' ++ Δ').
Proof. unfold env_order_refl. simpl. rewrite env_weight_app. lia. Qed.
Lemma env_order_refl_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ).
Proof. unfold env_order_refl. do 2 rewrite env_weight_add. lia. Qed.
Lemma env_order_refl_add' Δ Δ' φ φ': weight φ ≤ weight φ' -> (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ').
Proof. unfold env_order_refl. do 2 rewrite env_weight_add.
intros. apply Nat.add_le_mono. lia. apply Nat.pow_le_mono_r; lia. Qed.
Global Hint Resolve env_order_disj_union_compat_left : order.
Global Hint Resolve env_order_disj_union_compat_right : order.
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_3 : order.
Global Hint Resolve env_order_4 : order.
Global Hint Resolve env_order_5 : order.
Global Hint Resolve env_order_6 : order.
Global Hint Resolve env_order_7 : order.
Global Hint Resolve env_order_8 : order.
Global Hint Resolve env_order_add_compat : order.
Global Hint Resolve env_order_cancel_right : order.
Global Hint Resolve env_order_refl_cancel_right : order.
Global Hint Resolve env_order_cancel_left : order.
Global Hint Resolve env_order_refl_add : order.
Global Hint Resolve env_order_refl_add' : order.
Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order.
Ltac get_diff_form g := match g with
| ?Γ ∖{[?φ]} => φ
| _ (?Γ ∖{[?φ]}) => φ
| _ (rm ?φ _) => φ
| (rm ?φ _) => φ
| ?Γ ++ _ => get_diff_form Γ
| _ :: ?Γ => get_diff_form Γ
end.
Ltac get_diff_env g := match g with
| ?Γ ∖{[?φ]} => Γ
| _ :: ?Γ => get_diff_env Γ
end.
Lemma remove_env_order Δ φ: rm φ Δ ≼ Δ.
Proof.
unfold env_order_refl.
induction Δ as [|ψ Δ]. trivial.
simpl. destruct form_eq_dec; repeat rewrite env_weight_add; lia.
Qed.
Global Hint Resolve remove_env_order : order.
Lemma remove_In_env_order_refl Δ φ: In φ Δ -> rm φ Δ • φ ≼ Δ.
Proof.
induction Δ as [|ψ Δ].
- intro Hf; contradict Hf.
- intros [Heq | Hin].
+ subst. simpl. destruct form_eq_dec; [|tauto]. auto with order.
+ specialize (IHΔ Hin). simpl. case form_eq_dec as [Heq | Hneq].
* subst. auto with order.
* rewrite (Permutation_swap ψ φ (rm φ Δ)). auto with order.
Qed.
Global Hint Resolve remove_In_env_order_refl : order.
Lemma Permutation_rm φ Γ : φ ∈ Γ -> Γ ≡ₚ φ :: rm φ Γ.
Proof.
induction Γ as [| a Γ]; intro Hin.
- inversion Hin.
- simpl. case (form_eq_dec φ a).
+ intro; subst; trivial.
+ intro. rewrite Permutation_swap. auto with *.
Qed.
Lemma env_order_lt_le_trans Γ Γ' Γ'' : (Γ ≺ Γ') -> (Γ' ≼ Γ'') -> Γ ≺ Γ''.
Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
Lemma env_order_le_lt_trans Γ Γ' Γ'' : (Γ ≼ Γ') -> (Γ' ≺ Γ'') -> Γ ≺ Γ''.
Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
Lemma remove_In_env_order Δ φ: In φ Δ -> rm φ Δ ≺ Δ.
Proof.
intro Hin. apply remove_In_env_order_refl in Hin.
eapply env_order_lt_le_trans; [|apply Hin]. auto with order.
Qed.
Global Hint Resolve remove_In_env_order : order.
Lemma elem_of_list_In_1 {A : Type}: ∀ (l : list A) (x : A), x ∈ l <-> In x l.
Proof. apply elem_of_list_In. Qed.
Global Hint Resolve elem_of_list_In_1 : order.
Lemma elements_elem_of {Γ : env} {φ : form} :
φ ∈ Γ -> elements Γ ≡ₚ φ :: elements (Γ ∖ {[φ]}).
Proof.
intro Hin. setoid_rewrite <- elements_env_add.
apply Proper_elements, symmetry, difference_singleton, Hin.
Qed.
Lemma env_pair_order_cancel_right p Γ Δ Δ' : (p ≺· (Γ, Δ)) -> (p ≺· (Γ, Δ ++ Δ')).
Proof.
unfold env_pair_order. simpl. intro.
repeat rewrite app_assoc. apply env_order_cancel_right.
repeat rewrite <- app_assoc. rewrite (Permutation_app_comm Δ' Δ).
repeat rewrite app_assoc.
apply env_order_cancel_right.
repeat rewrite <- app_assoc. trivial.
Qed.
Lemma env_pair_order_cancel_left p Γ Δ Δ' : (p ≺· (Γ, Δ')) -> (p ≺· (Γ, Δ ++ Δ')).
Proof.
unfold env_pair_order. simpl. intro. rewrite (Permutation_app_comm Δ Δ').
apply env_pair_order_cancel_right, H.
Qed.
Ltac prepare_order :=
repeat (apply env_order_add_compat);
unfold env_pair_order; subst; simpl; repeat rewrite open_boxes_add; try multimatch goal with
| Δ := _ |- _ => subst Δ; try prepare_order
| Hin : ?a ∈ ?Γ |- context[elements ?Γ] => rewrite (elements_elem_of Hin); try prepare_order
| Hin' : ?b ∈ ?Γ, Hin : ?a ∈ ?Γ |- context[?Γ ++ ?Δ] => rewrite (Permutation_app_tail Δ (Permutation_rm _ _ Hin')); try prepare_order
| Hin : ?a ∈ ?Γ |- context[?Γ ++ ?Δ] => rewrite (Permutation_app_tail Δ (Permutation_rm _ _ Hin)); try prepare_order
| Hin : ?a ∈ ?Δ |- context[?Γ ++ ?Δ] => rewrite (Permutation_app_head Γ (Permutation_rm _ _ Hin)); try prepare_order
| H : _ ∈ list_to_set_disj _ |- _ => apply elem_of_list_to_set_disj in H; try prepare_order
| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ => let ψ' := (get_diff_form Γ') in
apply (env_order_equiv_right_compat (difference_singleton Γ ψ' H)) ||
(eapply env_order_lt_le_trans ; [| apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial])
| H : ?ψ ∈ ?Γ |- ?Γ' ≺ (?φ :: ?Γ) => let ψ' := (get_diff_form Γ') in
apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))
| H : ?ψ ∈ ?Γ |- ?Γ' ≺ (_ :: _ :: ?Γ) => let ψ' := (get_diff_form Γ') in
apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))) ||
(eapply env_order_le_lt_trans; [| apply env_order_add_compat;
eapply env_order_lt_le_trans; [| (apply env_order_refl_add; apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial) ] ] )
|H : ?a = _ |- context[?a] => rewrite H; try prepare_order
end.
Lemma openboxes_env_order Δ δ : (map open_box Δ) • δ • δ ≺ Δ • □ δ.
Proof.
induction Δ as [|x Δ].
- simpl. unfold env_order, ltof, env_weight. simpl.
repeat rewrite <- plus_n_O. apply Nat.add_lt_mono_l.
rewrite plus_n_O at 1. auto with *.
- apply (env_order_equiv_right_compat (Δ'' := Δ • □ δ • x)); [constructor|].
simpl.
eapply (env_order_equiv_left_compat (Δ'' := map open_box Δ • δ • δ • ⊙ x)).
+ do 2 (rewrite (Permutation_swap δ (⊙ x)); apply Permutation_skip). trivial.
+ dependent destruction x; intros; simpl; try (solve[now apply env_order_add_compat]).
transitivity (x :: (□δ) :: Δ).
* auto with *.
* apply env_order_1; simpl; auto. left.
Qed.
Lemma env_order_open_box Γ φ (Hin : (□ φ) ∈ Γ) : □⁻¹ Γ ≺ Γ.
Proof.
induction Γ as [|x Γ] ; cbn ; [ inversion Hin | ].
inversion Hin ; subst.
- cbn. apply env_order_1 ; cbn ; [ lia | apply open_boxes_env_order ].
- destruct x ; cbn ; try ( now apply env_order_add_compat ; auto).
apply env_order_1 ; [ cbn ; lia | apply env_order_env_order_refl ; auto].
Qed.
Global Hint Resolve env_order_open_box : order.
Global Hint Resolve openboxes_env_order : order.
Lemma weight_Arrow_1 φ ψ : 1 < weight (φ → ψ).
Proof. simpl. pose (weight_pos φ). lia. Qed.
Lemma weight_Box_1 φ: 1 < weight (□ φ).
Proof. simpl. pose (weight_pos φ). lia. Qed.
Global Hint Resolve weight_Arrow_1 : order.
Global Hint Resolve weight_Box_1 : order.
Lemma env_order_empty Δ : (elements (∅ : env)) ≼ Δ.
Proof.
unfold env_order_refl. setoid_rewrite gmultiset_elements_empty.
unfold env_weight. simpl. lia.
Qed.
Global Hint Resolve env_order_empty : order.
Ltac order_tac :=
try unfold env_pair_ms_order; prepare_order;
try replace (elements ∅) with ([] : list form) by ms;
repeat rewrite elements_open_boxes;
repeat rewrite env_replace by ms;
repeat rewrite env_add_remove;
repeat rewrite elements_env_add;
repeat rewrite Permutation_middle;
simpl; auto 10 with order;
repeat (apply env_order_disj_union_compat_right; order_tac).
Global Hint Extern 5 (?a ≺ ?b) => order_tac : proof.
Hint Extern 5 (?a ≺· ?b) => order_tac : proof.
Lemma env_pair_order_bot_R pe Δ Δ': (pe ≺· (Δ, [])) -> pe ≺· (Δ, Δ').
Proof.
intro Hlt. destruct pe as (Γ, ψ). unfold env_pair_order. simpl.
eapply env_order_lt_le_trans. exact Hlt. simpl.
unfold env_order_refl. repeat rewrite env_weight_add.
simpl. repeat rewrite env_weight_app, ?env_weight_nil. lia.
Qed.
Hint Resolve env_pair_order_bot_R : order.
Lemma env_pair_order_bot_L pe Δ φ: ((Δ, φ) ≺· pe) -> (Δ, []) ≺· pe.
Proof.
intro Hlt. destruct pe as (Γ, ψ). unfold env_pair_order. simpl.
eapply env_order_le_lt_trans; [|exact Hlt]. simpl.
unfold env_order_refl. repeat rewrite ?env_weight_app, ?env_weight_nil. lia.
Qed.
Lemma env_pair_order_botf_L pe Δ φ: ((Δ, φ) ≺· pe) -> (Δ, []) ≺· pe.
Proof.
intro Hlt. destruct pe as (Γ, ψ). unfold env_pair_order. simpl.
eapply env_order_le_lt_trans; [|exact Hlt]. simpl.
unfold env_order_refl. repeat rewrite ?env_weight_app, ?env_weight_nil. lia.
Qed.
Hint Resolve env_pair_order_bot_L : order.
Lemma weight_or_bot a b: weight(⊥) < weight (a ∨b).
Proof. destruct a; simpl; lia. Qed.
Hint Resolve weight_or_bot : order.
Definition env_pair_order_refl (pe1 : env_pair) (pe2 : env_pair) :=
env_order_refl (fst pe1 ++ snd pe1 ++ snd pe1) (fst pe2 ++ snd pe2 ++ snd pe2).
Lemma env_pair_order_l (Γ Γ' Δ : list form) : (Γ ≺ Γ') -> (Γ, Δ) ≺· (Γ', Δ).
Proof.
intro. unfold env_pair_order. simpl. now apply env_order_disj_union_compat_left.
Qed.
Hint Resolve env_pair_order_l : order.
Lemma env_pair_order_nil_l (Γ Γ' Δ : list form) : (Γ ≺ Γ') -> (Γ, []) ≺· (Γ', Δ).
Proof. unfold env_pair_order, env_order, ltof. simpl.
repeat rewrite env_weight_app, ?env_weight_nil. lia.
Qed.
Hint Resolve env_pair_order_nil_l : order.