From b9c90fc530904b0fd4371b2b040e7842afae2683 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 17 Jan 2024 10:26:03 +0100 Subject: [PATCH] first doc --- Makefile | 3 +- .../doc-config => doc-config}/footer.html | 0 .../doc-config => doc-config}/header.html | 0 .../resources/config.js | 0 .../resources/coqdoc.css | 0 .../resources/coqdocjs.css | 0 .../resources/coqdocjs.js | 0 html/ISL.Environments.html | 825 ++++++++++ html/ISL.Formulas.html | 233 +++ html/ISL.Order.html | 380 +++++ html/ISL.PropQuantifiers.html | 1109 +++++++++++++ html/ISL.SequentProps.html | 1336 ++++++++++++++++ html/ISL.Sequents.html | 305 ++++ html/config.js | 72 + html/coqdoc.css | 197 +++ html/coqdocjs.css | 249 +++ html/coqdocjs.js | 189 +++ html/indexpage.html | 1382 +++++++++++++++++ html/toc.html | 156 ++ 19 files changed, 6435 insertions(+), 1 deletion(-) rename {theories/doc-config => doc-config}/footer.html (100%) rename {theories/doc-config => doc-config}/header.html (100%) rename {theories/doc-config => doc-config}/resources/config.js (100%) rename {theories/doc-config => doc-config}/resources/coqdoc.css (100%) rename {theories/doc-config => doc-config}/resources/coqdocjs.css (100%) rename {theories/doc-config => doc-config}/resources/coqdocjs.js (100%) create mode 100644 html/ISL.Environments.html create mode 100644 html/ISL.Formulas.html create mode 100644 html/ISL.Order.html create mode 100644 html/ISL.PropQuantifiers.html create mode 100644 html/ISL.SequentProps.html create mode 100644 html/ISL.Sequents.html create mode 100644 html/config.js create mode 100644 html/coqdoc.css create mode 100644 html/coqdocjs.css create mode 100644 html/coqdocjs.js create mode 100644 html/indexpage.html create mode 100644 html/toc.html diff --git a/Makefile b/Makefile index e4bc8f5..02f99ba 100644 --- a/Makefile +++ b/Makefile @@ -4,6 +4,7 @@ COQDOCFLAGS:= \ --index indexpage --no-lib-name --parse-comments \ --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html export COQDOCFLAGS +PUBLIC_URL="..." _: makefile.coq @@ -12,7 +13,7 @@ makefile.coq: doc: makefile.coq rm -fr html - COQDOCEXTRAFLAGS='--external "https://ipq.gitlab.io/doc/"' + COQDOCEXTRAFLAGS='--external $(PUBLIC_URL)' @$(MAKE) -f makefile.coq html cp $(EXTRA_DIR)/resources/* html diff --git a/theories/doc-config/footer.html b/doc-config/footer.html similarity index 100% rename from theories/doc-config/footer.html rename to doc-config/footer.html diff --git a/theories/doc-config/header.html b/doc-config/header.html similarity index 100% rename from theories/doc-config/header.html rename to doc-config/header.html diff --git a/theories/doc-config/resources/config.js b/doc-config/resources/config.js similarity index 100% rename from theories/doc-config/resources/config.js rename to doc-config/resources/config.js diff --git a/theories/doc-config/resources/coqdoc.css b/doc-config/resources/coqdoc.css similarity index 100% rename from theories/doc-config/resources/coqdoc.css rename to doc-config/resources/coqdoc.css diff --git a/theories/doc-config/resources/coqdocjs.css b/doc-config/resources/coqdocjs.css similarity index 100% rename from theories/doc-config/resources/coqdocjs.css rename to doc-config/resources/coqdocjs.css diff --git a/theories/doc-config/resources/coqdocjs.js b/doc-config/resources/coqdocjs.js similarity index 100% rename from theories/doc-config/resources/coqdocjs.js rename to doc-config/resources/coqdocjs.js diff --git a/html/ISL.Environments.html b/html/ISL.Environments.html new file mode 100644 index 0000000..2375996 --- /dev/null +++ b/html/ISL.Environments.html @@ -0,0 +1,825 @@ + + + + + + + + + + + + + +
+
+

ISL.Environments

+ +
+
+ +
+

Overview: Environments

+ + +
+ + An environment is a multiset of formulas. The main role of this file is to + link up the multisets from IRIS's stdpp with the multisets from CoLoR: The + stdpp multisets provide useful tactics, while CoLoR proves that + well-foundedness of an ordering lifts to the set of multi-sets over that + order. +
+ + Notion of wellfoundedness +
+
+Require Import Coq.Program.Wf.
+ +
+
+ +
+Stdpp implementation of multisets +
+
+Require Export stdpp.gmultiset.
+ +
+
+ +
+Proof that ordering on multisets is wellfounded from CoLoR +
+
+Require Import CoLoR.Util.Multiset.MultisetOrder.
+Require Import CoLoR.Util.Multiset.MultisetCore.
+ +
+
+ +
+Our propositional formulas, including their countability. +
+
+Require Export ISL.Formulas.
+ +
+
+ +
+An environment is defined as a finite multiset of formulas +(in the sense of the stdpp library). +This requires decidable equality and countability of the underlying set. +
+
+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.
+ +
+
+ +
+

Connecting two kinds of multisets

+ We now show that our env is also a multiset in the sense of CoLoR, so that +we can use the wellfoundedness proof from CoLoR and the multiset tactics and +notations from stdpp. +
+
+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.
+ +
+
+ +
+

A well-founded order and tactic on multi-sets

+ The module MO defines the multi-set ordering on multi-sets, + which depends on giving an order on the base set (for us, formulas), + and, crucially, contains the wellfoundedness theorem "mord_wf". +
+
+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
+*)
+ +
+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.
+ +
+Global Notation "Γ • φ" := (disj_union Γ (base.singletonMS φ)) (at level 105, φ at level 85, left associativity).
+ +
+
+ +
+

Multiset utilities

+ +
+
+(* 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.
+ +
+
+ +
+

Conjunction, disjunction, and implication

+ In the construction of propositional quantifiers, we often want to take the conjunction, disjunction, or implication of a (multi)set of formulas. The following results give some small optimizations of this process, by reducing "obvious" conjunctions such as ⊤ ∧ ϕ, ⊥ ∧ ϕ, etc. +
+
+ +
+Definition irreducible (Γ : env) :=
+  (∀ p φ, (Var p → φ) ∈ Γ -> ¬ Var p ∈ Γ) /\
+  ¬ ⊥ ∈ Γ /\
+  ∀ φ ψ, ¬ (φ ∧ ψ) ∈ Γ /\ ¬ (φ ∨ ψ) ∈ Γ.
+ +
+
+ +
+We use binary conjunction and disjunction operations which produce simpler equivalent formulas, + in particular by taking ⊥ and ⊤ into account +
+
+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 :=
+if decide (x = ⊥) then ⊤ else if decide (y = (⊥ → ⊥)) then ⊤ else x → y.
+ +
+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.
+ +
+
+ +
+To be noted: we remove duplicates first +
+
+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 version of `map`

+ +
+
+(* 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.
+ +
+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.
+ +
+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.
+ +
+(* 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).
+ +
+
+ +
+

Tactics

+ +
+
+(* 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.
+ +
+Definition open_box φ : form := match φ with
+| □ φ => φ
+| φ => φ
+end.
+ +
+(* inefficient conversion from multisets to lists and back *)
+Definition open_boxes (Γ : env) : env := list_to_set_disj (map open_box (elements Γ)).
+ +
+Global Notation "⊙ φ" := (open_box φ) (at level 75).
+Global Notation "⊗ Γ" := (open_boxes Γ) (at level 75).
+ +
+Global Instance proper_open_boxes : Proper ((≡@{env}) ==> (≡@{env})) open_boxes.
+Proof. intros Γ Heq Δ Heq'. ms. Qed.
+ +
+Lemma open_boxes_empty : open_boxes ∅ = ∅.
+Proof. auto. Qed.
+ +
+Lemma open_boxes_disj_union (Γ : env) Δ : (open_boxes (Γ ⊎ Δ)) = (open_boxes Γ ⊎ open_boxes Δ).
+Proof.
+unfold open_boxes. rewrite (gmultiset_elements_disj_union Γ Δ).
+rewrite map_app. apply list_to_set_disj_app.
+Qed.
+ +
+Lemma open_boxes_singleton φ : open_boxes {[φ]} = {[⊙ φ]}.
+Proof.
+unfold open_boxes.
+assert (HH := gmultiset_elements_singleton φ).
+unfold elements, base.singletonMS, singletonMS, base.singleton, Environments.singleton in *.
+rewrite HH. simpl. ms.
+Qed.
+ +
+Lemma open_boxes_add (Γ : env) φ : (open_boxes (Γ • φ)) = (open_boxes Γ • open_box φ).
+Proof.
+rewrite open_boxes_disj_union.
+unfold open_boxes. f_equal. apply open_boxes_singleton.
+Qed.
+ +
+Lemma elem_of_open_boxes φ Δ : φ ∈ (⊗Δ) -> φ ∈ Δ \/ (□φ) ∈ Δ.
+Proof.
+intro Hin.
+induction Δ as [|θ Δ Hind] using gmultiset_rec.
+- auto with proof.
+- rewrite open_boxes_disj_union in Hin.
+  apply gmultiset_elem_of_disj_union in Hin.
+  destruct Hin as [Hθ | HΔ].
+  + rewrite open_boxes_singleton in Hθ. apply gmultiset_elem_of_singleton in Hθ.
+      subst φ. destruct θ; ms.
+  + destruct (Hind HΔ); ms.
+Qed.
+ +
+Lemma occurs_in_open_boxes x φ Δ : occurs_in x φ -> φ ∈ (⊗Δ) -> exists θ, θ ∈ Δ /\ occurs_in x θ.
+Proof.
+intros Hx Hφ. apply elem_of_open_boxes in Hφ. destruct Hφ as [Hφ|Hφ]; eauto.
+Qed.
+ +
+Global Hint Rewrite open_boxes_disj_union : proof.
+ +
+Global Instance open_boxes_equiv : Proper (equiv ==> equiv) open_boxes.
+Proof. intros Γ Γ'. ms. Qed.
+ +
+Lemma open_boxes_remove Γ φ : φ ∈ Γ -> (≡@{env}) (⊗ (Γ ∖ {[φ]})) ((⊗ Γ) ∖ {[⊙ φ]}).
+Proof.
+intro Hin. rewrite (difference_singleton Γ φ Hin) at 2.
+rewrite open_boxes_add. ms.
+Qed.
+ +
+Definition is_box φ := match φ with
+| □ _ => true
+| _ => false
+end.
+ +
+Lemma open_boxes_spec Γ φ : φ ∈ open_boxes Γ -> {φ ∈ Γ ∧ is_box φ = false} + {(□ φ) ∈ Γ}.
+Proof.
+unfold open_boxes. intro Hin. apply elem_of_list_to_set_disj in Hin.
+apply elem_of_list_In in Hin. apply ListUtil.in_map_elim in Hin.
+case (decide ((□ φ) ∈ Γ)).
+- right; trivial.
+- intro Hout. left.
+  destruct Hin as (y & Hin & Hy). subst.
+  destruct y; simpl in *; split; trivial;
+  try (apply gmultiset_elem_of_elements,elem_of_list_In; trivial);
+  contradict Hout; apply gmultiset_elem_of_elements,elem_of_list_In; trivial.
+Qed.
+ +
+Lemma is_not_box_open_box φ : is_box φ = false -> (⊙φ) = φ.
+Proof. destruct φ; simpl; intuition. discriminate. Qed.
+ +
+Lemma open_boxes_spec' Γ φ : {φ ∈ Γ ∧ is_box φ = false} + {(□ φ) ∈ Γ} -> φ ∈ open_boxes Γ.
+Proof.
+intros [[Hin Heq] | Hin];
+unfold open_boxes; apply elem_of_list_to_set_disj, elem_of_list_In, in_map_iff.
+- exists φ. apply is_not_box_open_box in Heq. rewrite Heq. split; trivial.
+  now apply elem_of_list_In, gmultiset_elem_of_elements.
+- exists (□ φ). simpl. split; trivial. now apply elem_of_list_In, gmultiset_elem_of_elements.
+Qed.
+ +
+Lemma In_open_boxes (Γ : env) (φ : form) : (φ ∈ Γ) -> open_box φ ∈ open_boxes Γ.
+Proof.
+intro Hin. apply difference_singleton in Hin.
+eapply (proper_elem_of _ _ eq_refl _ (open_boxes (Γ ∖ {[φ]} • φ))).
+- now apply open_boxes_equiv.
+- rewrite open_boxes_add. auto with *.
+Qed.
+ +
+Global Hint Resolve In_open_boxes : proof.
+Global Hint Unfold open_box : proof.
+Global Hint Rewrite open_boxes_empty : proof.
+Global Hint Rewrite open_boxes_add : proof.
+Global Hint Rewrite open_boxes_remove : proof.
+Global Hint Rewrite open_boxes_singleton : proof.
+ +
+Global Hint Resolve open_boxes_spec' : proof.
+Global Hint Resolve open_boxes_spec : proof.
+ +
+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
+|H1 : ?x0 ∈ (⊗ ?Δ), H2 : occurs_in ?x ?x0 |- _ =>
+      apply (occurs_in_open_boxes _ _ _ H2) in H1
+end;
+repeat match goal with | H : exists x, _ |- _ => destruct H end; intuition;
+try multimatch goal with
+| H : ?θ0 ∈ ?Δ0 |- context [exists θ, θ ∈ ?Δ /\ occurs_in ?x θ] =>
+  solve[try right; exists θ0; split; [eauto using difference_include|simpl; tauto]; eauto] end.
+
+
+ +
+ + + diff --git a/html/ISL.Formulas.html b/html/ISL.Formulas.html new file mode 100644 index 0000000..4784b14 --- /dev/null +++ b/html/ISL.Formulas.html @@ -0,0 +1,233 @@ + + + + + + + + + + + + + +
+
+

ISL.Formulas

+ +
+
+ +
+

Overview: formulas

+ + +
+ +This file defines propositional formulas, the proof that there are countably many, and the definition of the well-founded ordering on the set of formulas, via weight. +
+ + Theory of countability from Iris +
+
+From stdpp Require Import countable.
+ +
+
+ +
+

Definitions and notations.

+ +
+
+Definition variable := nat.
+ +
+Inductive form : Type :=
+| Var : variable -> form
+| Bot : form
+| And : form -> form -> form
+| Or : form -> form -> form
+| Implies : form -> form -> form
+| Box : form -> form.
+ +
+Fixpoint occurs_in (x : variable) (φ : form) :=
+match φ with
+| Var y => x = y
+| Bot => False
+| And φ ψ => (occurs_in x φ) \/ (occurs_in x ψ)
+| Or φ ψ => (occurs_in x φ) \/ (occurs_in x ψ)
+| Implies φ ψ => (occurs_in x φ) \/ (occurs_in x ψ)
+| Box φ => occurs_in x φ
+
+end.
+ +
+
+ +
+Pretty notations for formulas +
+
+Notation "¬ φ" := (Implies φ Bot) (at level 75, φ at level 75).
+Notation " ⊥ " := Bot.
+Notation " ⊤ " := (Implies Bot Bot).
+Notation " A ∧ B" := (And A B) (at level 80, B at level 80).
+Notation " A ∨ B" := (Or A B) (at level 85, B at level 85).
+Notation " A → B" := (Implies A B) (at level 99, B at level 200).
+Notation "□ φ" := (Box φ) (at level 75, φ at level 75).
+Infix " φ ⇔ ψ " := (And (Implies φ ψ) (Implies ψ φ)) (at level 100).
+Global Instance fomula_bottom : base.Bottom form := Bot.
+ +
+Global Coercion Var : variable >-> form.
+ +
+Global Instance form_top : base.Top form := ⊤.
+ +
+
+ +
+Formulas have decidable equality. +
+
+Global Instance form_eq_dec : EqDecision form.
+Proof. solve_decision. Defined.
+ +
+Section CountablyManyFormulas.
+
+ +
+

Countability of the set of formulas

+ We prove that there are countably many formulas by exhibiting an injection + into general trees over nat for countability. +
+
+Local Fixpoint form_to_gen_tree (φ : form) : gen_tree nat :=
+match φ with
+| ⊥ => GenLeaf 0
+| Var v => GenLeaf (1 + v)
+| φ ∧ ψ => GenNode 0 [form_to_gen_tree φ ; form_to_gen_tree ψ]
+| φ ∨ ψ => GenNode 1 [form_to_gen_tree φ ; form_to_gen_tree ψ]
+| φ → ψ => GenNode 2 [form_to_gen_tree φ ; form_to_gen_tree ψ]
+| □ φ => GenNode 3 [form_to_gen_tree φ]
+end.
+ +
+Local Fixpoint gen_tree_to_form (t : gen_tree nat) : option form :=
+match t with
+| GenLeaf 0 => Some ⊥
+| GenLeaf (S n) => Some (Var n)
+| GenNode 0 [t1 ; t2] =>
+    gen_tree_to_form t1 ≫= fun φ => gen_tree_to_form t2 ≫= fun ψ =>
+      Some (φ ∧ ψ)
+| GenNode 1 [t1 ; t2] =>
+    gen_tree_to_form t1 ≫= fun φ => gen_tree_to_form t2 ≫= fun ψ =>
+      Some (φ ∨ ψ)
+| GenNode 2 [t1 ; t2] =>
+    gen_tree_to_form t1 ≫= fun φ => gen_tree_to_form t2 ≫= fun ψ =>
+      Some (φ → ψ)
+ | GenNode 3 [t] => gen_tree_to_form t ≫= fun φ => Some (□φ)
+| _=> None
+end.
+ +
+Global Instance form_count : Countable form.
+Proof.
+  apply inj_countable with (f := form_to_gen_tree) (g := gen_tree_to_form).
+  intro φ; induction φ; simpl; trivial; now rewrite IHφ1, IHφ2 || rewrite IHφ.
+Defined.
+ +
+End CountablyManyFormulas.
+ +
+Inductive subform : form -> form -> Prop :=
+| SubEq : ∀ φ, subform φ φ
+| SubAnd : ∀ φ ψ1 ψ2, (subform φ ψ1 + subform φ ψ2) -> subform φ (ψ1 ∧ ψ2)
+| SubOr : ∀ φ ψ1 ψ2, (subform φ ψ1 + subform φ ψ2) -> subform φ (ψ1 ∨ ψ2)
+| SubImpl : ∀ φ ψ1 ψ2, (subform φ ψ1 + subform φ ψ2) -> subform φ (ψ1→ ψ2)
+| SubBox : ∀ φ ψ, subform φ ψ -> subform φ (□ ψ).
+Local Hint Constructors subform : dyckhoff.
+ +
+
+ +
+

Weight

+ + +
+ +We define the weight function on formulas, following (Dyckhoff Negri 2000) +
+
+Fixpoint weight (φ : form) : nat := match φ with
+| ⊥ => 1
+| Var _ => 1
+| φ ∧ ψ => 2 + weight φ + weight ψ
+| φ ∨ ψ => 3 + weight φ + weight ψ
+| φ → ψ => 1 + weight φ + weight ψ
+| □φ => 1 + weight φ
+end.
+ +
+Lemma weight_pos φ : weight φ > 0.
+Proof. induction φ; simpl; lia. Qed.
+ +
+
+ +
+We obtain an induction principle based on weight. +
+
+Definition weight_ind (P : form -> Type) :
+ (forall ψ, (∀ φ, (weight φ < weight ψ) -> P φ) -> P ψ) ->
+ (∀ φ, P φ).
+Proof.
+  intros Hc φ. remember (weight φ) as w.
+  assert(Hw : weight φ ≤ w) by now subst. clear Heqw.
+  revert φ Hw. induction w; intros φ Hw.
+  - pose (Hw' := weight_pos φ). auto with *.
+  - destruct φ; simpl in Hw; trivial;
+    apply Hc; intros φ' Hw'; apply IHw; simpl in Hw'; lia.
+Defined.
+ +
+Definition form_order φ ψ := weight φ > weight ψ.
+ +
+Global Instance transitive_form_order : Transitive form_order.
+Proof. unfold form_order. auto with *. Qed.
+ +
+Global Instance irreflexive_form_order : Irreflexive form_order.
+Proof. unfold form_order. intros x y. lia. Qed.
+ +
+Notation "φ ≺f ψ" := (form_order ψ φ) (at level 149).
+
+
+ +
+ + + diff --git a/html/ISL.Order.html b/html/ISL.Order.html new file mode 100644 index 0000000..bf72236 --- /dev/null +++ b/html/ISL.Order.html @@ -0,0 +1,380 @@ + + + + + + + + + + + + + +
+
+

ISL.Order

+ +
+Require Export ISL.Environments.
+ +
+Definition env_order (Γ Δ : env): Prop := MO.MultisetGt form_order Δ Γ.
+Infix "≺" := env_order (at level 150).
+ +
+Notation "Δ ≼ Δ'" := ((Δ ≺ Δ') \/ Δ ≡ Δ') (at level 150).
+ +
+Global Hint Unfold form_order : mset.
+ +
+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.
+ +
+
+ +
+Here we use the theorem of (Dershowitz Manna 1979), formalized in CoLoR as mord_wf, which says that the multiset ordering over a well-founded + ordering (in our case, the one given by formula weight) is again well-founded. +
+
+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.
+ +
+(* 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 {φ}. *)
+ (* TODO: modified from G4IP : right-hand side counts twice, to account for the right box rule. Is this working? *)
+Definition pointed_env_order (pe1 : pointed_env) (pe2 : pointed_env) :=
+  env_order (fst pe1 • snd pe1 • snd pe1) (fst pe2 • snd 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.
+ +
+Infix "≺·" := pointed_env_order (at level 150).
+ +
+Lemma env_order_equiv_right_compat {Δ Δ' Δ'' : env}:
+  Δ' ≡ Δ'' ->
+  (Δ ≺ Δ'') ->
+  Δ ≺ Δ'.
+Proof. ms. Qed.
+ +
+Lemma env_order_equiv_left_compat {Δ Δ' Δ'' : env}:
+  Δ ≡ Δ'' ->
+  (Δ'' ≺ Δ') ->
+  Δ ≺ Δ'.
+Proof. ms. Qed.
+ +
+Global Instance Proper_env_order : Proper ((≡@{env}) ==> (≡@{env}) ==> (fun x y => x <-> y)) env_order.
+Proof. intros Δ1 Δ2 H12 Δ3 Δ4 H34; ms. 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.
+ +
+Lemma env_order_compat Δ Δ' φ1 φ : weight φ1 < weight φ -> (Δ' ≼ Δ) -> Δ' • φ1 ≺ Δ • φ.
+Proof.
+intros Hw [Hlt | Heq].
+- transitivity (Δ' • φ); auto using env_order_1 with *.
+  apply mord_ext_r; auto with *. apply irreflexive_form_order.
+- subst. rewrite Heq. now apply env_order_1.
+Qed.
+ +
+Global Hint Resolve env_order_compat : order.
+ +
+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.
+ +
+(* TODO: this is just a special case *)
+Lemma env_order_disj_union_compat_left Δ Δ' Δ'':
+  (Δ ≺ Δ'') -> Δ ⊎ Δ' ≺ Δ'' ⊎ Δ'.
+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.
+ +
+Lemma env_order_disj_union_compat_right Δ Δ' Δ'':
+  (Δ ≺ Δ'') -> Δ' ⊎ Δ ≺ Δ' ⊎ Δ''.
+Proof.
+intro H. eapply (Proper_env_order _ (Δ ⊎ Δ') _ _ (Δ'' ⊎ Δ')) . ms.
+now apply env_order_disj_union_compat_left.
+Unshelve. ms.
+Qed.
+ +
+Lemma env_order_disj_union_compat Δ Δ' Δ'' Δ''':
+  (Δ ≺ Δ'') -> (Δ' ≺ Δ''') -> Δ ⊎ Δ' ≺ Δ'' ⊎ Δ'''.
+Proof.
+intros H1 H2.
+transitivity (Δ ⊎ Δ''').
+- now apply env_order_disj_union_compat_right.
+- now apply env_order_disj_union_compat_left.
+Qed.
+ +
+Lemma env_order_disj_union_compat_strong_right Δ Δ' Δ'' Δ''':
+  (Δ ≺ Δ'') -> (Δ' ≼ Δ''') -> Δ ⊎ Δ' ≺ Δ'' ⊎ Δ'''.
+Proof.
+intros H1 H2.
+destruct H2 as [Hlt|Heq].
+- apply Operators_Properties.clos_rt_t with (Δ'' ⊎ Δ').
+  + apply RelUtil.tc_incl_rtc. now apply env_order_disj_union_compat_right.
+  + now apply env_order_disj_union_compat_left.
+- rewrite Heq. now apply env_order_disj_union_compat_left.
+Qed.
+ +
+(*
+Lemma open_box_env_order(φ : form) : ({+ ⊙φ +} ≺ {+ φ +}) \/ ({+ ⊙ φ +} = {+ φ +}).
+Proof.
+
+Qed.
+*)
+Lemma open_boxes_env_order Δ : (⊗Δ) ≼ Δ.
+Proof.
+induction Δ as [|φ Δ] using gmultiset_rec.
+- right. autorewrite with proof. auto.
+- destruct IHΔ as [Hlt | Heq].
+  + left. autorewrite with proof. eapply (Proper_env_order _ ((⊗Δ) • ⊙φ) _ _ (Δ•φ)). ms.
+      apply env_order_disj_union_compat_strong_right. trivial.
+      destruct φ; simpl; try ms. left. (* TODO: lemme *)
+      eapply (Proper_env_order _ (∅ • φ) _ _ (∅•□φ) _ ). Unshelve. all: try ms.
+      apply env_order_1. simpl. lia.
+  + rewrite open_boxes_disj_union, open_boxes_singleton, Heq.
+      case_eq (is_box φ); intro Hbox; simpl.
+      * left. apply env_order_disj_union_compat_strong_right; [|ms].
+         destruct φ; simpl in *; try inversion Hbox.
+         eapply (Proper_env_order _ (∅ • φ) _ _ (∅•□φ) _ ). Unshelve. all: try ms. apply env_order_1. simpl. lia.
+      * right. destruct φ; simpl in *; ms.
+Qed.
+ +
+Global Hint Resolve open_boxes_env_order : order.
+ +
+Global Instance assoc_meq_union : Assoc meq union.
+Proof. intros x y z. ms. 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.
+ +
+(* TODO: ok? to replace env_order_* ?
+Lemma env_order_l (Δ' Δ: env) φ1 φ: weight φ1 < weight φ -> (Δ' ≺ Δ • φ) -> (Δ' • φ1) ≺ (Δ • φ).
+Proof.
+*)
+ +
+Lemma env_order_2 Δ Δ' φ1 φ2 φ: weight φ1 < weight φ -> weight φ2 < weight φ ->
+  (Δ' ≼ Δ) -> Δ' • φ1 • φ2 ≺ Δ • φ.
+Proof.
+intros Hw1 Hw2 Hor.
+eapply (Proper_env_order _ ((∅ • φ1 • φ2) ⊎ Δ') _ _ ((∅ • φ) ⊎ Δ)) . ms.
+apply env_order_disj_union_compat_strong_right; trivial.
+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.
+Unshelve. ms.
+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.
+eapply (Proper_env_order _ ((∅ • φ1 • φ2 • φ3) ⊎ Δ') _ _ ((∅ • φ) ⊎ Δ)) . ms.
+apply env_order_disj_union_compat_strong_right; trivial.
+constructor. eapply MSetRed with (Y := ∅ • φ1 • φ2 • φ3); [reflexivity| |].
+- ms.
+- intros y Hy.
+  repeat (apply MSet.member_union in Hy; destruct Hy as [Hy|Hy];
+  [|apply MSet.member_singleton in Hy; now rewrite Hy]).
+  apply MSet.not_empty in Hy; ms.
+Unshelve. ms.
+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.
+eapply (Proper_env_order _ ((∅ • φ1 • φ2 • φ3 • φ4) ⊎ Δ') _ _ ((∅ • φ) ⊎ Δ)) . ms.
+apply env_order_disj_union_compat_strong_right; trivial.
+constructor. eapply MSetRed with (Y := ∅ • φ1 • φ2 • φ3 • φ4); [reflexivity| |].
+- ms.
+- intros y Hy.
+  repeat (apply MSet.member_union in Hy; destruct Hy as [Hy|Hy];
+  [|apply MSet.member_singleton in Hy; now rewrite Hy]).
+  apply MSet.not_empty in Hy; ms.
+Unshelve. ms.
+Qed.
+ +
+Lemma env_order_cancel_right Δ Δ' φ: (Δ ≺ Δ') -> Δ ≺ (Δ' • φ).
+Proof. etransitivity; [|apply env_order_0]. assumption. Qed.
+ +
+Lemma env_order_eq_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ).
+Proof. intros[Heq|Hlt]. left. now apply env_order_add_compat. right. ms. 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_3 : order.
+Global Hint Resolve env_order_4 : order.
+Global Hint Resolve env_order_add_compat : order.
+Global Hint Resolve env_order_cancel_right : order.
+Global Hint Resolve env_order_eq_add : order.
+Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order.
+ +
+Ltac get_diff_form g := match g with
+| ?Γ ∖{[?φ]} => φ
+| _ (?Γ ∖{[?φ]}) => φ
+| ?Γ • _ => get_diff_form Γ
+end.
+ +
+Ltac get_diff_env g := match g with
+| ?Γ ∖{[?φ]} => Γ
+| ?Γ • _ => get_diff_env Γ
+end.
+ +
+Global Hint Rewrite open_boxes_remove : order.
+ +
+Ltac prepare_order :=
+repeat (apply env_order_add_compat);
+unfold pointed_env_order; subst; simpl; repeat rewrite open_boxes_add; try match goal with
+| Δ := _ |- _ => subst Δ; try prepare_order
+| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ => let ψ' := (get_diff_form Γ') in
+    apply (env_order_equiv_right_compat (difference_singleton Γ ψ' H))
+| 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))))
+end.
+(*
+Global Hint Extern 2 ((?Γ  ∖ {?ψ} , ?φ) ≺· (?Γ, ?φ)) => prepare_order : order.
+Global Hint Extern 2 (?Γ  ∖ {?ψ} • ?φ' • ?φ'' ≺ ?Γ • ?φ) => prepare_order : order.
+Global Hint Extern 2 (?Γ  ∖ {?ψ} • ?φ' • ?φ'' ≺ ?Γ • ?φ • ?φ''') => prepare_order : order.
+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.
+- assert (H := weight_pos ψ). lia.
+- 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 Nat.le_lt_trans; [eapply make_impl_weight|]) : order.
+ +
+Global Hint Extern 5 (weight (?φ ⇢ (?ψ ⇢ ?θ)) < _) => (eapply Nat.le_lt_trans; [eapply make_impl_weight2|]) : order.
+ +
+(* TODO: new *)
+ +
+(* ad hoc *)
+Lemma openboxes_env_order Δ δ : (⊗ Δ) • δ • δ ≺ Δ • □ δ.
+Proof.
+induction Δ using gmultiset_rec.
+- eapply @env_order_equiv_left_compat with (∅ • δ • δ).
+  + now rewrite open_boxes_empty.
+  + apply env_order_2; simpl; try lia. ms.
+- apply (@env_order_equiv_right_compat _ _ (Δ • □ δ • x)); [ms|].
+  eapply (@env_order_equiv_left_compat _ _ (⊗ Δ • δ • δ • ⊙ x)).
+  rewrite open_boxes_disj_union, open_boxes_singleton. ms.
+  case x; intros; simpl; try (solve[now apply env_order_add_compat]).
+  transitivity (Δ • □δ • f).
+  + auto with *.
+  + apply env_order_1. simpl. auto.
+Qed.
+ +
+Global Hint Resolve openboxes_env_order : order.
+ +
+Ltac order_tac := prepare_order; auto 10 with order.
+ +
+
+
+ +
+ + + diff --git a/html/ISL.PropQuantifiers.html b/html/ISL.PropQuantifiers.html new file mode 100644 index 0000000..60e9c9c --- /dev/null +++ b/html/ISL.PropQuantifiers.html @@ -0,0 +1,1109 @@ + + + + + + + + + + + + + +
+
+

ISL.PropQuantifiers

+ +
+Require Import ISL.Sequents.
+Require Import ISL.SequentProps ISL.Order.
+Require Import Coq.Program.Equality. (* for dependent induction *)
+ +
+
+ +
+

Overview: Propositional Quantifiers

+ + +
+ +The main theorem proved in this file was first proved as Theorem 1 in: + +
+ +(Pitts 1992). A. M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log., 57(1):33–52. + +
+ +It consists of two parts: + +
+ +1) the inductive construction of the propositional quantifiers; + +
+ +2) a proof of its correctness. +
+
+ +
+Section Pitts.
+ +
+
+ +
+Throughout the construction and proof, we fix a variable p, with respect to + which the propositional quantifier will be computed. +
+
+Variable p : variable.
+ +
+
+ +
+

Definition of propositional quantifiers.

+ +
+
+ +
+Section PropQuantDefinition.
+ +
+
+ +
+We define the formulas Eφ and Aφ associated to any formula φ. This + is an implementation of Pitts' Table 5, together with a (mostly automatic) + proof that the definition terminates. +
+
+ +
+(* solves the obligations of the following programs *)
+Obligation Tactic := intros; order_tac.
+ +
+
+ +
+First, the implementation of the rules for calculating E. The names of the rules + refer to the table in Pitts' paper. note the use of "lazy" conjunctions, disjunctions and implications +
+
+Program Definition e_rule {Δ : env} {ϕ : form}
+  (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form)
+  (θ: form) (Hin : θ ∈ Δ) : form :=
+let E Δ H := fst (EA0 (Δ, ϕ) H) in
+let A pe0 H := snd (EA0 pe0 H) in
+let Δ' := Δ ∖ {[θ]} in
+match θ with
+| Bot => ⊥ (* E0 *)
+| Var q =>
+    if decide (p = q) then ⊤ (* default *)
+    else E Δ' _ ⊼ q (* E1 *)
+(* E2 *)
+| δ₁ ∧ δ₂ => E ((Δ'•δ₁)•δ₂) _
+(* E3 *)
+| δ₁ ∨ δ₂ => E (Δ'•δ₁) _ ⊻ E (Δ' •δ₂) _
+| Var q → δ =>
+    if decide (p = q)
+    then
+      if decide (Var p ∈ Δ) then E (Δ'•δ) _ (* E5 *)
+      else ⊤
+    else q ⇢ E (Δ'•δ) _ (* E4 *)
+(* E6 *)
+| (δ₁ ∧ δ₂)→ δ₃ => E (Δ'•(δ₁ → (δ₂ → δ₃))) _
+(* E7 *)
+| (δ₁ ∨ δ₂)→ δ₃ => E (Δ'•(δ₁ → δ₃)•(δ₂ → δ₃)) _
+(* E8 *)
+| ((δ₁→ δ₂)→ δ₃) =>
+  (E (Δ'•(δ₂ → δ₃)) _⇢ A (Δ'•(δ₂ → δ₃), δ₁ → δ₂) _) ⇢ E (Δ'•δ₃) _
+| Bot → _ => ⊤
+| □ φ => □(E ((⊗Δ') • φ ) _) (* very redundant ; identical for each box *)
+| (□δ1 → δ2) => (□(E((⊗Δ') • δ2 • □δ1) _ → A((⊗Δ') • δ2 • □δ1, δ1) _) → E(Δ' • δ2) _)
+end. (* TODO: E((⊗Δ') • δ2 • □δ1) _) →  ? *)
+(* TODO lemma : E(Δ) |- θ -> E(⊗Δ) ⊢ θ *)
+ +
+
+ +
+The implementation of the rules for defining A is separated into two pieces. + Referring to Table 5 in Pitts, the definition a_rule_env handles A1-8 and A10, + and the definition a_rule_form handles A9 and A11-13. +
+
+Program Definition a_rule_env {Δ : env} {ϕ : form}
+  (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form)
+  (θ: form) (Hin : θ ∈ Δ) : form :=
+let E Δ H := fst (EA0 (Δ, ϕ) H) in
+let A pe0 H := snd (EA0 pe0 H) in
+let Δ' := Δ ∖ {[θ]} in
+match θ with
+| Var q =>
+    if decide (p = q)
+    then
+      if decide (Var p = ϕ) then ⊤ (* A10 *)
+      else ⊥
+    else A (Δ', ϕ) _ (* A1 *)
+(* A2 *)
+| δ₁ ∧ δ₂ => A ((Δ'•δ₁)•δ₂, ϕ) _
+(* A3 *)
+| δ₁ ∨ δ₂ =>
+      (E (Δ'•δ₁) _ ⇢ A (Δ'•δ₁, ϕ) _)
+  ⊼ (E (Δ'•δ₂) _ ⇢ A (Δ'•δ₂, ϕ) _)
+| Var q → δ =>
+    if decide (p = q)
+    then
+      if decide (Var p ∈ Δ) then A (Δ'•δ, ϕ) _ (* A5 *)
+      else ⊥
+    else q ⊼ A (Δ'•δ, ϕ) _ (* A4 *)
+(* A6 *)
+| (δ₁ ∧ δ₂)→ δ₃ =>
+  A (Δ'•(δ₁ → (δ₂ → δ₃)), ϕ) _
+(* A7 *)
+| (δ₁ ∨ δ₂)→ δ₃ =>
+  A ((Δ'•(δ₁ → δ₃))•(δ₂ → δ₃), ϕ) _
+(* A8 *)
+| ((δ₁→ δ₂)→ δ₃) =>
+  (E (Δ'•(δ₂ → δ₃)) _ ⇢ A (Δ'•(δ₂ → δ₃), (δ₁ → δ₂)) _)
+  ⊼ A (Δ'•δ₃, ϕ) _
+| Bot => ⊥
+| Bot → _ => ⊥
+| □δ => ⊥
+| ((□δ1) → δ2) => □(E((⊗Δ')• δ2 • □δ1) _ → A((⊗Δ')• δ2 • □δ1, δ1) _) ∧ A(Δ' • δ2, ϕ) _
+(* TODO: (E((⊗Δ') • δ2 • □δ1)  _ → ? *)
+end.
+ +
+(* make sure that the proof obligations do not depend on EA0 *)
+Obligation Tactic := intros Δ ϕ _ _ _; intros; order_tac.
+Program Definition a_rule_form {Δ : env} {ϕ : form}
+  (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) : form :=
+let E pe0 H := fst (EA0 pe0 H) in
+let A pe0 H := snd (EA0 pe0 H) in
+match ϕ with
+| Var q =>
+    if decide (p = q)
+    then ⊥
+    else Var q (* A9 *)
+(* A11 *)
+| ϕ₁ ∧ ϕ₂ => A (Δ, ϕ₁) _ ⊼ A (Δ, ϕ₂) _
+(* A12 *)
+| ϕ₁ ∨ ϕ₂ => A (Δ, ϕ₁) _ ⊻ A (Δ, ϕ₂) _
+(* A13 *)
+| ϕ₁→ ϕ₂ => E (Δ•ϕ₁, ϕ₂) _ ⇢ A (Δ•ϕ₁, ϕ₂) _
+| Bot => ⊥
+| □δ => □((E ((⊗Δ) • □δ, δ) _) ⇢ A((⊗Δ) • □δ, δ) _)
+end.
+ +
+Obligation Tactic := intros; order_tac.
+Program Fixpoint EA (pe : env * form) {wf pointed_env_order pe} :=
+  let Δ := fst pe in
+  (⋀ (in_map Δ (e_rule EA)),
+   ⋁ (in_map Δ (a_rule_env EA)) ⊻ a_rule_form EA).
+Next Obligation. apply wf_pointed_order. Defined.
+ +
+Definition E (pe : env * form) := (EA pe).1.
+Definition A (pe : env * form) := (EA pe).2.
+ +
+Definition Ef (ψ : form) := E ({[ψ]}, ⊥).
+Definition Af (ψ : form) := A (∅, ψ).
+ +
+
+ +
+Congruence lemmas: if we apply any of e_rule, a_rule_env, or a_rule_form + to two equal environments, then they give the same results. +
+
+Lemma e_rule_cong Δ ϕ θ (Hin : θ ∈ Δ) EA1 EA2:
+  (forall pe Hpe, EA1 pe Hpe = EA2 pe Hpe) ->
+  @e_rule Δ ϕ EA1 θ Hin = @e_rule Δ ϕ EA2 θ Hin.
+Proof.
+  intro Heq.
+  destruct θ; simpl; try (destruct θ1); repeat (destruct decide);
+  f_equal; repeat erewrite Heq; trivial.
+Qed.
+ +
+Lemma a_rule_env_cong Δ ϕ θ Hin EA1 EA2:
+  (forall pe Hpe, EA1 pe Hpe = EA2 pe Hpe) ->
+  @a_rule_env Δ ϕ EA1 θ Hin = @a_rule_env Δ ϕ EA2 θ Hin.
+Proof.
+  intro Heq.
+  destruct θ; simpl; trivial; repeat (destruct decide);
+  f_equal; repeat erewrite Heq; trivial;
+  destruct θ1; try (destruct decide); trivial;
+  repeat erewrite Heq; trivial.
+Qed.
+ +
+Lemma a_rule_form_cong Δ ϕ EA1 EA2:
+  (forall pe Hpe, EA1 pe Hpe = EA2 pe Hpe) ->
+  @a_rule_form Δ ϕ EA1 = @a_rule_form Δ ϕ EA2.
+Proof.
+  intro Heq.
+  destruct ϕ; simpl; repeat (destruct decide); trivial;
+  repeat (erewrite Heq; eauto); trivial.
+Qed.
+ +
+
+ +
+The following lemma requires proof irrelevance due to in_map. +
+
+Lemma EA_eq Δ ϕ:
+  (E (Δ, ϕ) = ⋀ (in_map Δ (@e_rule Δ ϕ (λ pe _, EA pe)))) /\
+  (A (Δ, ϕ) = (⋁ (in_map Δ (@a_rule_env Δ ϕ (λ pe _, EA pe)))) ⊻
+       @a_rule_form Δ ϕ (λ pe _, EA pe)).
+Proof.
+simpl. unfold E, A, EA. simpl.
+rewrite -> Wf.Fix_eq.
+- simpl. split; trivial.
+- intros Δ' f g Heq. f_equal; f_equal.
+  + apply in_map_ext. intros. apply e_rule_cong; intros; f_equal.
+      now rewrite Heq.
+  + f_equal. apply in_map_ext. intros. apply a_rule_env_cong; intros.
+      now rewrite Heq.
+  + apply a_rule_form_cong; intros. now rewrite Heq.
+Qed.
+ +
+Definition E_eq Δ ϕ := proj1 (EA_eq Δ ϕ).
+Definition A_eq Δ ϕ := proj2 (EA_eq Δ ϕ).
+ +
+End PropQuantDefinition.
+ +
+
+ +
+

Correctness

+ +
+
+Section Correctness.
+ +
+
+ +
+This section contains the proof of Proposition 5, the main correctness result, stating that the E- and A-formulas defined above are indeed existential and universal propositional quantified versions of the original formula, respectively. +
+ +

(i) Variables

+ +
+
+Section VariablesCorrect.
+ +
+
+ +
+In this subsection we prove (i), which states that the variable p no longer + occurs in the E- and A-formulas, and that the E- and A-formulas contain no more variables than the original formula. + +
+ +

(a)

+ +
+
+ +
+Lemma e_rule_vars (Δ : env) (θ : form) (Hin : θ ∈ Δ) (ϕ : form)
+  (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) x
+  (HEA0 : ∀ pe Hpe,
+      (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\
+      (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))) :
+occurs_in x (e_rule EA0 θ Hin) -> x ≠ p ∧ ∃ θ, θ ∈ Δ /\ occurs_in x θ.
+Proof.
+destruct θ; unfold e_rule.
+- case decide.
+  + simpl. intros Heq HF; subst. tauto.
+  + simpl. intros Hneq Hocc. apply occurs_in_make_conj in Hocc.
+      destruct Hocc as [Hocc|Heq]; vars_tac. subst; tauto.
+- simpl. tauto.
+- vars_tac.
+- intro Hocc. apply occurs_in_make_disj in Hocc as [Hocc|Hocc]; vars_tac.
+- destruct θ1; try solve[vars_tac].
+  + case decide.
+    * intro; subst. case decide.
+      -- vars_tac.
+      -- simpl; tauto.
+    * intros Hneq Hocc. apply occurs_in_make_impl in Hocc as [Heq | Hocc]; vars_tac.
+      subst. tauto.
+  + intros Hocc. apply occurs_in_make_impl in Hocc.
+      destruct Hocc as [Hocc|Hocc]; [apply occurs_in_make_impl in Hocc as [Hocc|Hocc]|]; vars_tac; subst; tauto.
+  + intros Hocc; repeat destruct Hocc as [Hocc|Hocc]; simpl in Hocc; vars_tac.
+- intuition; simpl in *; vars_tac.
+Qed.
+
+ +
+

(b)

+ +
+
+ +
+Lemma a_rule_env_vars Δ θ Hin ϕ
+  (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) x
+  (HEA0 : ∀ pe Hpe,
+      (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\
+      (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))):
+occurs_in x (a_rule_env EA0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ).
+Proof.
+destruct θ; unfold a_rule_env.
+- case decide.
+  + intro; subst. case decide; simpl; tauto.
+  + intros Hneq Hocc. vars_tac.
+- simpl. tauto.
+- intro Hocc. vars_tac.
+- intros Hocc. apply occurs_in_make_conj in Hocc.
+  destruct Hocc as [Hocc|Hocc];
+  apply occurs_in_make_impl in Hocc; vars_tac; vars_tac.
+- destruct θ1; try solve[vars_tac].
+  + case decide.
+    * intro; subst. case decide.
+      -- intros Hp Hocc. vars_tac.
+      -- simpl; tauto.
+    * intros Hneq Hocc. apply occurs_in_make_conj in Hocc.
+       destruct Hocc as [Heq | Hocc]; vars_tac. subst; tauto.
+  + intros Hocc. apply occurs_in_make_conj in Hocc.
+      destruct Hocc as [Hocc|Hocc].
+      * apply occurs_in_make_impl in Hocc; vars_tac; vars_tac.
+      * vars_tac.
+  + intros Hocc. try apply occurs_in_make_impl in Hocc.
+      destruct Hocc as [Hocc|Hocc].
+      * try apply occurs_in_make_conj in Hocc; vars_tac; vars_tac.
+      * vars_tac.
+- simpl; tauto.
+Qed.
+ +
+Lemma a_rule_form_vars Δ ϕ
+  (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) x
+  (HEA0 : ∀ pe Hpe,
+      (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\
+      (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))):
+  occurs_in x (a_rule_form EA0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ).
+Proof.
+destruct ϕ.
+- simpl. case decide; simpl; intros; subst; intuition; auto.
+- tauto.
+- simpl. intros Hocc; apply occurs_in_make_conj in Hocc as [Hocc|Hocc]; vars_tac.
+- simpl. intros Hocc; apply occurs_in_make_disj in Hocc as [Hocc|Hocc]; vars_tac.
+- simpl. intro Hocc. apply occurs_in_make_impl in Hocc. destruct Hocc; vars_tac; vars_tac.
+- intro Hocc. replace (occurs_in x (□ ϕ)) with (occurs_in x ϕ) by trivial.
+  unfold a_rule_form in Hocc. (* apply occurs_in_make_impl in Hocc. *)
+  repeat vars_tac; eauto using occurs_in_open_boxes.
+Qed.
+ +
+Proposition EA_vars Δ ϕ x:
+  (occurs_in x (E (Δ, ϕ)) -> x <> p /\ ∃ θ, θ ∈ Δ /\ occurs_in x θ) /\
+  (occurs_in x (A (Δ, ϕ)) -> x <> p /\ (occurs_in x ϕ \/ (∃ θ, θ ∈ Δ /\ occurs_in x θ))).
+Proof.
+remember (Δ, ϕ) as pe.
+replace Δ with pe.1 by now subst.
+replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. revert pe.
+refine (@well_founded_induction _ _ wf_pointed_order _ _).
+intros [Δ ϕ] Hind. simpl.
+rewrite E_eq, A_eq. simpl.
+split.
+(* E *)
+- intros Hocc. apply variables_conjunction in Hocc as (φ&Hin&Hφ).
+  apply in_in_map in Hin as (ψ&Hin&Heq). subst φ.
+  apply e_rule_vars in Hφ.
+  + trivial.
+  + intros; now apply Hind.
+(* A *)
+- intro Hocc. apply occurs_in_make_disj in Hocc as [Hocc|Hocc].
+  (* disjunction *)
+  + apply variables_disjunction in Hocc as (φ&Hin&Hφ).
+      apply in_in_map in Hin as (ψ&Hin&Heq). subst φ.
+      apply a_rule_env_vars in Hφ; trivial.
+  (* pointer rule *)
+  + apply a_rule_form_vars in Hocc.
+    * destruct Hocc as [Hneq [Hocc | Hocc]]; vars_tac.
+    * vars_tac; apply Hind in H; trivial; tauto.
+Qed.
+ +
+End VariablesCorrect.
+ +
+Ltac foldEA := repeat match goal with
+| |- context C [(EA ?pe).1] => fold (E pe)
+| |- context C [(EA ?pe).2] => fold (A pe)
+end.
+ +
+
+ +
+

(ii) Entailment

+ +
+
+Section EntailmentCorrect.
+ +
+
+ +
+In this section we prove (ii), which states that the E- and A-formula are + entailed by the original formula and entail the original formula, + respectively. +
+
+ +
+Hint Extern 5 (?a ≺ ?b) => order_tac : proof.
+Opaque make_disj.
+Opaque make_conj.
+ +
+Lemma a_rule_env_spec Δ θ ϕ Hin (EA0 : ∀ pe, (pe ≺· (Δ, ϕ)) → form * form)
+  (HEA : forall Δ ϕ Hpe, (Δ ⊢ fst (EA0 (Δ, ϕ) Hpe)) * (Δ• snd(EA0 (Δ, ϕ) Hpe) ⊢ ϕ)) :
+  (Δ•a_rule_env EA0 θ Hin ⊢ ϕ).
+Proof with (auto with proof).
+assert (HE := λ Δ0 ϕ0 Hpe, fst (HEA Δ0 ϕ0 Hpe)).
+assert (HA := λ Δ0 ϕ0 Hpe, snd (HEA Δ0 ϕ0 Hpe)).
+clear HEA.
+destruct θ; exhibit Hin 1.
+- simpl; case decide; intro Hp.
+  + subst. case_decide; subst; auto with proof.
+  + exch 0...
+- constructor 2.
+- simpl; exch 0. apply AndL. exch 1; exch 0...
+- apply make_conj_sound_L.
+  exch 0. apply OrL; exch 0.
+  + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L... (* uses imp_cut *)
+  + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L. auto with proof.
+- destruct θ1.
+  + simpl; case decide; intro Hp.
+    * subst. case decide.
+      -- intros Hp.
+         assert(Hin' : (p → θ2) ∈ Δ ∖ {[Var p]})
+         by (rewrite (gmultiset_disj_union_difference' _ _ Hp) in Hin; ms).
+         assert (Hin'' : Var p ∈ Δ ∖ {[p → θ2]}) by now apply in_difference.
+         exhibit Hin'' 2. exch 0; exch 1. apply ImpLVar.
+         exch 1. exch 0. peapply HA. rewrite <- difference_singleton by trivial. reflexivity.
+      -- intro; constructor 2.
+    * apply make_conj_sound_L. constructor 4. exch 0. exch 1. exch 0. apply ImpLVar.
+      exch 0. apply weakening. exch 0...
+  + constructor 2.
+  + simpl; exch 0. apply ImpLAnd. apply make_impl_complete_L2. exch 0...
+  + simpl; exch 0. apply ImpLOr. exch 1. exch 0...
+  + apply make_conj_sound_L. exch 0. apply ImpLImp; exch 0.
+      * apply AndL...
+      * apply AndL. exch 0. apply weakening, HA.
+  + exch 0. simpl. exch 0. apply AndL. exch 1; exch 0. apply ImpBox.
+      * box_tac. box_tac. exch 0; exch 1; exch 0. apply weakening. exch 1; exch 0. apply ImpL.
+         -- auto with proof.
+         -- apply HA.
+      * exch 1; exch 0. apply weakening. exch 0. auto with proof.
+- auto with proof.
+Qed.
+ +
+Proposition entail_correct Δ ϕ : (Δ ⊢ E (Δ, ϕ)) * (Δ•A (Δ, ϕ) ⊢ ϕ).
+Proof.
+remember (Δ, ϕ) as pe.
+replace Δ with pe.1 by now subst.
+replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. revert pe.
+refine (@well_founded_induction _ _ wf_pointed_order _ _).
+unfold pointed_env_order.
+intros (Δ, ϕ) Hind. simpl.
+rewrite E_eq, A_eq.
+(* uncurry the induction hypothesis for convenience *)
+assert (HE := fun d f x=> fst (Hind (d, f) x)).
+assert (HA := fun d f x=> snd (Hind (d, f) x)).
+unfold E, A in *; simpl in HE, HA.
+simpl in *. clear Hind.
+split. {
+(* E *)
+apply conjunction_R1. intros φ Hin. apply in_in_map in Hin.
+destruct Hin as (ψ&Hin&Heq). subst.
+destruct ψ; unfold e_rule; exhibit Hin 0.
+- case decide; intro; subst; simpl; auto using HE with proof.
+- auto with proof.
+- auto 3 with proof.
+- apply make_disj_sound_R, OrL.
+  + apply OrR1, HE. order_tac.
+  + apply OrR2, HE. order_tac.
+- destruct ψ1; auto 3 using HE with proof.
+  + case decide; intro Hp.
+    * subst. case decide; intro Hp.
+      -- assert(Hin'' : Var p ∈ Δ ∖ {[p → ψ2]}) by (apply in_difference; trivial; discriminate).
+         exhibit Hin'' 1. apply ImpLVar.
+         peapply (HE (Δ ∖ {[p → ψ2]}•ψ2) ϕ). auto with proof.
+         rewrite <- difference_singleton; trivial.
+      -- apply ImpR, ExFalso.
+    * apply make_impl_sound_R, ImpR. exch 0. apply ImpLVar. exch 0. apply weakening, HE. order_tac.
+  + remember (Δ ∖ {[(ψ1_1 → ψ1_2) → ψ2]}) as Δ'.
+      apply make_impl_sound_R, ImpR. apply make_impl_sound_L. exch 0. apply ImpLImp.
+      * exch 0. auto with proof.
+      * exch 0. auto with proof.
+  + foldEA. apply ImpR. exch 0. apply ImpBox.
+         -- box_tac. exch 0; exch 1; exch 0. apply ImpL.
+            ++ apply weakening, HE. order_tac.
+            ++ apply HA. order_tac.
+         -- exch 0; apply weakening, HE. order_tac.
+- apply BoxR. apply weakening. box_tac. simpl. apply HE. order_tac.
+}
+(* A *)
+apply make_disj_sound_L, OrL.
+- apply disjunction_L. intros φ Hin.
+  apply in_in_map in Hin as (φ' & Heq & Hφ'). subst φ.
+  apply a_rule_env_spec; intros; split ; apply HE || apply HA; order_tac.
+- destruct ϕ; simpl; auto using HE with proof.
+  + case decide; intro; subst; [constructor 2|constructor 1].
+  + apply make_conj_sound_L, AndR; apply AndL; auto using HE with proof.
+  + apply ImpR. exch 0. apply make_impl_sound_L, ImpL; auto using HE, HA with proof.
+  + foldEA. apply BoxR. box_tac. exch 0. apply make_impl_sound_L, ImpL.
+      * apply weakening, HE. order_tac.
+      * apply HA. order_tac.
+Qed.
+ +
+End EntailmentCorrect.
+ +
+
+ +
+

Uniformity

+ +
+
+Section PropQuantCorrect.
+ +
+
+ +
+The proof in this section, which is the most complex part of the argument, + shows that the E- and A-formulas constructed above are indeed their propositionally quantified versions, that is, *any* formula entailed by the original formula and + using only variables from that formula except p is already a consequence of + the E-quantified version, and similarly on the other side for the A-quantifier. + +
+ + E's second argument is mostly irrelevant and is only there for uniform treatment with A +
+
+Lemma E_irr ϕ' Δ ϕ : E (Δ, ϕ) = E (Δ, ϕ').
+Proof.
+remember ((Δ, ϕ) : pointed_env) as pe.
+replace Δ with pe.1 by now subst.
+replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ.
+  induction pe as [[Γ φ] Hind0] using (well_founded_induction_type wf_pointed_order).
+assert(Hind : ∀ Γ0 φ0, ((Γ0, φ0) ≺· (Γ, φ)) → E (Γ0, φ0) = E (Γ0, ϕ'))
+  by exact (fun Γ0 φ0 => (Hind0 (Γ0, φ0))).
+unfold E in Hind. simpl in Hind.
+do 2 rewrite E_eq. f_equal. apply in_map_ext.
+intros φ' Hin. unfold e_rule.
+destruct φ'; repeat rewrite (Hind _ φ) by (trivial; order_tac); trivial.
+destruct φ'1; repeat rewrite (Hind _ φ) by (trivial; order_tac); trivial.
+Qed.
+ +
+Lemma E_left {Γ} {θ} {Δ} {φ φ'} (Hin : φ ∈ Δ) :
+(Γ•e_rule (λ pe (_ : pe ≺· (Δ, φ')), EA pe) φ Hin) ⊢ θ ->
+Γ•E (Δ, φ') ⊢ θ.
+Proof.
+intro Hp. rewrite E_eq.
+destruct (@in_map_in _ _ _ (e_rule (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule].
+eapply conjunction_L.
+- apply Hrule.
+- exact Hp.
+Qed.
+ +
+Lemma A_right {Γ} {Δ} {φ φ'} (Hin : φ ∈ Δ) :
+Γ ⊢ a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe) φ Hin ->
+Γ ⊢ A (Δ, φ').
+Proof. intro Hp. rewrite A_eq.
+destruct (@in_map_in _ _ _ (a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule].
+eapply make_disj_sound_R, OrR1, disjunction_R.
+- exact Hrule.
+- exact Hp.
+Qed.
+ +
+(* TODO: move *)
+Lemma open_boxes_case Δ : {φ | (□ φ) ∈ Δ} + {Δ ≡ ⊗Δ}.
+Proof.
+unfold open_boxes.
+induction Δ as [|ψ Δ IH] using gmultiset_rec.
+- right. ms.
+- case_eq(is_box ψ); intro Hbox.
+  + left. exists (⊙ψ).
+      destruct ψ; try discriminate Hbox. ms.
+  + destruct IH as [[φ Hφ]| Heq].
+     * left. exists φ. ms.
+     * right. symmetry. etransitivity.
+        -- apply env_equiv_eq, list_to_set_disj_perm, Permutation_map.
+            apply gmultiset_elements_disj_union.
+        -- rewrite map_app, list_to_set_disj_app. rewrite <- Heq. apply env_equiv_eq.
+            f_equal.
+            unfold elements. apply is_not_box_open_box in Hbox. rewrite <- Hbox at 2.
+            transitivity (list_to_set_disj (map open_box (id [ψ])) : env).
+            ++ apply list_to_set_disj_perm, Permutation_map.
+                    apply Permutation_refl', gmultiset_elements_singleton.
+            ++ simpl. ms.
+Qed.
+ +
+Proposition pq_correct Γ Δ ϕ: (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> (Γ ⊎ Δ ⊢ ϕ) ->
+  (¬ occurs_in p ϕ -> Γ•E (Δ, ϕ) ⊢ ϕ) *
+  (Γ•E (Δ, ϕ) ⊢ A (Δ, ϕ)).
+Proof.
+(* we want to use an E rule *)
+Ltac Etac := foldEA; intros; match goal with | Hin : ?a ∈ ?Δ |- _•E (?Δ, _) ⊢ _=> apply (E_left Hin); unfold e_rule end.
+ +
+(* we want to use an A rule defined in a_rule_env *)
+Ltac Atac := foldEA; match goal with | Hin : ?a ∈ ?Δ |- _ ⊢ A (?Δ, _) => apply (A_right Hin); unfold a_rule_env end.
+ +
+(* we want to use an A rule defined in a_rule_form *)
+Ltac Atac' := foldEA; rewrite A_eq; apply make_disj_sound_R, OrR2; simpl.
+ +
+Ltac occ := simpl; tauto ||
+match goal with
+| Hnin : ∀ φ0 : form, φ0 ∈ ?Γ → ¬ occurs_in p φ0 |- _ =>
+
+  let Hin := fresh "Hin" in
+  try (match goal with |Hocc : ?a ∈ ?Γ |- _ => let Hocc' := fresh "Hocc" in assert (Hocc' := Hnin _ Hocc); simpl in Hocc';
+  let Hin' := fresh "Hinx" in assert(Hin' := In_open_boxes _ _ Hocc); simpl in *;
+  try rewrite open_boxes_remove in * by trivial end);
+  intro; repeat rewrite env_in_add; repeat rewrite difference_include; simpl;
+  intro Hin; try tauto;
+  try (destruct Hin as [Hin|[Hin|Hin]] ||destruct Hin as [Hin|Hin]);
+  subst; simpl; try tauto;
+  repeat (apply difference_include in Hin; [|assumption]);
+  try (now apply Hnin)
+end.
+ +
+Ltac equiv_tac :=
+multimatch goal with
+| Heq' : _•_ ≡ _ |- _ => fail
+| Heq' : _ ≡ _ |- _ ≡ _ =>
+  try (rewrite <- difference_singleton; trivial);
+  rewrite Heq';
+  try (rewrite union_difference_L by trivial);
+  try (rewrite union_difference_R by trivial);
+  try ms
+end.
+ +
+intros Hnin Hp.
+remember (Γ ⊎ Δ) as Γ' eqn:HH.
+assert (Heq: Γ' ≡ Γ ⊎ Δ) by ms. clear HH.
+revert Heq.
+dependent induction Hp generalizing Γ Δ Hnin; intro Heq;
+try (apply env_add_inv in Heq; [|discriminate]);
+
+(* try and solve the easy case where the main formula is on the left *)
+try match goal with
+| H : (?Γ0•?a•?b) ≡ Γ ⊎ Δ |- _ => idtac
+| H : (?Γ0•?a) ≡ Γ ⊎ Δ |- _ => rename H into Heq;
+  assert(Hin : a ∈ (Γ0•a)) by ms; rewrite Heq in Hin;
+  pose(Heq' := Heq); apply env_add_inv' in Heq';
+  try (case (decide (a ∈ Γ)); intro Hin0;
+  [split; intros; exhibit Hin0 1|
+   case (decide (a ∈ Δ)); intro Hin0';
+  [|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto]])
+end; simpl.
+ +
+(* Atom *)
+- auto 2 with proof.
+- Atac'. case decide; intro; subst; [exfalso; now apply (Hnin _ Hin0)|]; auto with proof.
+- split; Etac; case decide; intro; subst; try tauto; auto with proof.
+  + Atac. repeat rewrite decide_True by trivial. auto with proof.
+  + fold E. apply make_conj_sound_L, AndL. Atac. repeat rewrite decide_False by trivial.
+    Atac'. rewrite decide_False by trivial. apply Atom.
+(* ExFalso *)
+- auto 2 with proof.
+- auto 2 with proof.
+- split; Etac; auto with proof.
+(* AndR *)
+- destruct (IHHp1 _ _ Hnin Heq) as (PE & PEA).
+  destruct (IHHp2 _ _ Hnin Heq) as (PE' & PEA').
+  split.
+  + intro Hocc. simpl in Hocc.
+    apply AndR; erewrite E_irr; apply IHHp2 || apply IHHp1; tauto.
+  + Atac'. apply make_conj_sound_R, AndR; erewrite E_irr; eassumption.
+(* AndL *)
+- exch 0. apply AndL. exch 1; exch 0. apply IHHp; trivial. occ. equiv_tac.
+- exch 0. apply AndL. exch 1; exch 0. apply IHHp; trivial. occ. equiv_tac.
+- split.
+   + Etac. apply IHHp; auto. equiv_tac.
+   + Atac. Etac. apply IHHp; auto. equiv_tac.
+(* OrR1 & OrR2 *)
+- split.
+  + intro Hocc. apply OrR1. erewrite E_irr; apply IHHp; tauto.
+  + rewrite A_eq. apply make_disj_sound_R, OrR2.
+      apply make_disj_sound_R, OrR1; erewrite E_irr.
+      apply IHHp; auto.
+- simpl. split.
+  + intro Hocc. apply OrR2. erewrite E_irr; apply IHHp; tauto.
+  + rewrite A_eq. apply make_disj_sound_R, OrR2.
+       apply make_disj_sound_R, OrR2; erewrite E_irr.
+       apply IHHp; auto.
+(* OrL *)
+- exch 0. apply OrL; exch 0.
+ + apply IHHp1; trivial. occ. equiv_tac.
+ + apply IHHp2; trivial. occ. equiv_tac.
+- exch 0. apply OrL; exch 0.
+  + apply IHHp1. occ. equiv_tac.
+  + apply IHHp2. occ. equiv_tac.
+- split.
+  + Etac. apply make_disj_sound_L, OrL; [apply IHHp1| apply IHHp2]; trivial;
+      rewrite Heq', union_difference_R by trivial; ms.
+  + Atac. apply weakening. apply make_conj_sound_R,AndR, make_impl_sound_R.
+    * apply make_impl_sound_R, ImpR. apply IHHp1; [tauto|equiv_tac].
+    * apply ImpR. apply IHHp2; [tauto|equiv_tac].
+(* ImpR *)
+- destruct (IHHp Γ (Δ•φ)) as [IHa IHb]; [auto|ms|].
+  split.
+  + intro Hocc. apply ImpR. exch 0.
+    erewrite E_irr. apply IHHp; auto. ms. equiv_tac.
+  + Atac'. auto with proof.
+(* ImpLVar *)
+- pose(Heq' := Heq); apply env_add_inv' in Heq'.
+  pose(Heq'' := Heq'); apply env_add_inv' in Heq''.
+  case (decide ((Var p0 → φ) ∈ Γ)).
+  + intro Hin0.
+    assert (Hocc' := Hnin _ Hin0). simpl in Hocc'.
+    case (decide (Var p0 ∈ Γ)); intro Hin1.
+    * (* subcase 1: p0, (p0 → φ) ∈ Γ *)
+      assert (Hin2 : Var p0 ∈ Γ ∖ {[Var p0 → φ]}) by (apply in_difference; trivial; discriminate).
+      split; [intro Hocc|];
+      exhibit Hin0 1; exhibit Hin2 2; exch 0; exch 1; apply ImpLVar; exch 1; exch 0;
+      (peapply IHHp; trivial; [occ|equiv_tac]).
+    * assert(Hin0' : Var p0 ∈ (Γ0•Var p0•(p0 → φ))) by ms. rewrite Heq in Hin0'.
+      case (decide (Var p0 ∈ Δ)); intro Hp0;
+      [|apply gmultiset_elem_of_disj_union in Hin0'; exfalso; tauto].
+      (* subcase 3: p0 ∈ Δ ; (p0 → φ) ∈ Γ *)
+      split; [Etac|Atac]; case decide; intro; subst.
+      -- tauto.
+      -- exhibit Hin0 1. apply make_conj_sound_L, AndL. exch 1; exch 0. apply ImpLVar. exch 1. exch 0.
+         apply IHHp; [occ|equiv_tac|trivial].
+      -- tauto.
+      -- exhibit Hin0 1. Etac. rewrite decide_False by trivial.
+         apply make_conj_sound_L, AndL. exch 1; exch 0. apply ImpLVar.
+         exch 1; exch 0. apply IHHp. occ. equiv_tac.
+  + intro.
+    assert(Hin : (Var p0 → φ) ∈ (Γ0•Var p0•(p0 → φ))) by ms.
+    rewrite Heq in Hin.
+    case (decide ((Var p0 → φ) ∈ Δ)); intro Hin0;
+    [|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto].
+    case (decide (Var p0 ∈ Γ)); intro Hin1.
+    * (* subcase 2: p0 ∈ Γ ; (p0 → φ) ∈ Δ *)
+      do 2 exhibit Hin1 1.
+      split; [intro Hocc|].
+      -- Etac. case_decide; [auto with *|].
+         apply make_impl_sound_L, ImpLVar. apply IHHp; trivial. occ.
+         rewrite Heq', union_difference_R, <- union_difference_L by trivial; ms.
+      -- Etac. case_decide; [auto with *|].
+         apply make_impl_sound_L, ImpLVar. Atac. repeat case_decide; auto 2 with proof; [tauto| tauto|].
+         apply make_conj_sound_R, AndR; auto 2 with proof. apply IHHp; [occ|].
+         rewrite Heq', union_difference_R, <- union_difference_L by trivial; ms.
+    * assert(Hin': Var p0 ∈ Γ ⊎ Δ) by (rewrite <- Heq; ms).
+      apply gmultiset_elem_of_disj_union in Hin'.
+      case (decide (Var p0 ∈ Δ)); intro Hin1'; [|exfalso; tauto].
+      (* subcase 4: p0,(p0 → φ) ∈ Δ *)
+      case (decide (p = p0)); intro.
+      -- (* subsubcase p = p0 *)
+        subst. split; Etac; repeat rewrite decide_True by trivial.
+        ++ apply IHHp; [tauto|equiv_tac|trivial].
+        ++ Atac. repeat rewrite decide_True by trivial.
+           apply IHHp; [tauto|equiv_tac].
+      -- (* subsubcase p ≠ p0 *)
+         assert ((p0 → φ) ∈ (Δ ∖ {[Var p0]})) by (apply in_difference; trivial; discriminate).
+         assert((Γ0•Var p0•φ) ≡ (Γ•Var p0) ⊎ (Δ ∖ {[Var p0]} ∖ {[p0 → φ]}•φ)). {
+          rewrite (assoc disj_union).
+          apply equiv_disj_union_compat_r.
+          rewrite (comm disj_union Γ {[Var p0]}).
+          rewrite <- (assoc disj_union).
+          rewrite (comm disj_union {[Var p0]}).
+          apply equiv_disj_union_compat_r.
+          rewrite Heq''.
+          rewrite union_difference_R by trivial.
+          rewrite union_difference_R. ms.
+          apply in_difference. discriminate. trivial.
+         } (* not pretty *)
+         split; Etac; rewrite decide_False by trivial;
+         apply make_conj_sound_L, AndL; exch 0; Etac; case decide; intro; try tauto.
+         ++ apply make_impl_sound_L, ImpLVar. apply IHHp; trivial. occ.
+         ++ Atac. case decide; intro; try tauto.
+            apply make_impl_sound_L, ImpLVar. Atac; case decide; intro; try tauto.
+            apply make_conj_sound_R, AndR; auto 2 with proof.
+            apply IHHp; trivial. occ.
+(* ImpLAnd *)
+- exch 0. apply ImpLAnd. exch 0. apply IHHp; trivial; [occ|equiv_tac].
+- exch 0. apply ImpLAnd. exch 0. apply IHHp; trivial; [occ|equiv_tac].
+- split; Etac.
+  + apply IHHp; trivial. equiv_tac.
+  + Atac. simpl. apply IHHp; trivial. equiv_tac.
+(* ImpLOr *)
+- exch 0; apply ImpLOr. exch 1; exch 0. apply IHHp; [occ|equiv_tac|trivial].
+- exch 0; apply ImpLOr. exch 1; exch 0. apply IHHp; [occ|equiv_tac].
+- split; Etac.
+  + apply IHHp; trivial. equiv_tac.
+  + Atac. apply IHHp; [occ|equiv_tac].
+(* ImpLImp *)
+- (* subcase 1: ((φ1 → φ2) → φ3) ∈ Γ *)
+  assert(ψ ≠ Var p) by (intro; subst; simpl in *; tauto).
+  exch 0; apply ImpLImp; exch 0.
+  + erewrite E_irr. apply IHHp1; [occ|equiv_tac|].
+      simpl. apply Hnin in Hin0. simpl in *. tauto.
+  + erewrite E_irr. apply IHHp2; [occ|equiv_tac|trivial].
+- exch 0; apply ImpLImp; exch 0.
+  + assert(IH: (Γ0•(φ2 → φ3)) ≡ (Γ ∖ {[(φ1 → φ2) → φ3]}•(φ2 → φ3)) ⊎ Δ) by equiv_tac.
+    erewrite E_irr. apply IHHp1; [occ|equiv_tac| trivial].
+    simpl. apply Hnin in Hin0. simpl in Hin0. tauto.
+  + apply IHHp2; [occ|equiv_tac].
+- (* subcase 2: ((φ1 → φ2) → φ3) ∈ Δ *)
+  split.
+  + Etac. apply make_impl_sound_L2'. apply ImpLImp.
+    * apply weakening. apply ImpR. foldEA.
+       rewrite (E_irr (φ1 → φ2)). apply IHHp1; [occ|equiv_tac].
+    * apply IHHp2; [occ|equiv_tac| trivial].
+  + Atac. apply make_conj_sound_R, AndR.
+    * apply weakening. apply make_impl_sound_R, ImpR. foldEA.
+      rewrite (E_irr (φ1 → φ2)). apply IHHp1; [occ|equiv_tac].
+    * Etac. simpl. apply make_impl_sound_L2', ImpLImp.
+      -- apply weakening. apply ImpR. foldEA.
+          rewrite (E_irr (φ1 → φ2)). apply IHHp1; [occ|equiv_tac].
+      -- apply IHHp2. occ. equiv_tac.
+- (* ImpBox, external *)
+   destruct (open_boxes_case Δ) as [[θ Hθ] | Hequiv].
+    + apply contraction. Etac. exch 1; exch 0; apply ImpBox.
+        * box_tac. box_tac. exch 2; exch 1; exch 0. apply weakening. foldEA.
+           erewrite E_irr with (ϕ' := φ1).
+           exch 1; exch 0.
+           apply IHHp1.
+           -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ).
+               apply (Hnin θ0); ms.
+           -- rewrite Heq'. assert(Hθ' := In_open_boxes _ _ Hθ).
+              simpl in *. repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union.
+              simpl. rewrite <- difference_singleton by trivial.
+              assert((□ φ1 → φ2) ∈ ⊗Γ) by auto with proof. rewrite union_difference_L by trivial. ms.
+          -- intro HF. apply (Hnin _ Hin0). simpl. tauto.
+        * exch 0. apply weakening. exch 0. apply IHHp2; [occ|equiv_tac| trivial].
+  + exch 0. apply ImpBox.
+      * box_tac. exch 1; exch 0. apply open_box_L.
+         erewrite E_irr with (ϕ' := φ1).
+         apply IHHp1.
+         -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ).
+             apply (Hnin θ0); ms.
+         -- rewrite Hequiv, Heq'. assert(Hθ' := In_open_boxes _ _ Hin0).
+             repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union.
+              simpl. rewrite union_difference_L by trivial. ms.
+         -- intro HF. apply (Hnin _ Hin0). simpl. tauto.
+     * exch 0. apply IHHp2; [occ | rewrite Heq'; equiv_tac | trivial].
+- destruct (open_boxes_case Δ) as [[θ Hθ] | Hequiv].
+    + apply contraction. Etac. exch 1; exch 0; apply ImpBox.
+        * box_tac. box_tac. exch 2; exch 1; exch 0. apply weakening. foldEA.
+           erewrite E_irr with (ϕ' := φ1).
+           exch 1; exch 0.
+           apply IHHp1.
+         -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ).
+             apply (Hnin θ0); ms.
+         -- rewrite Heq'. assert(Hθ' := In_open_boxes _ _ Hin0).
+             repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union.
+              simpl. rewrite union_difference_L by trivial.
+              rewrite <- difference_singleton by auto with proof. ms.
+         -- intro HF. apply (Hnin _ Hin0). simpl. tauto.
+        * exch 0. apply weakening. exch 0. apply IHHp2 ; [occ|equiv_tac].
+  + erewrite E_irr with (ϕ' := φ1).
+      exch 0. apply ImpBox.
+      * box_tac. exch 1; exch 0. apply open_box_L. apply IHHp1.
+         -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ).
+             apply (Hnin θ0); ms.
+         -- rewrite Heq'. assert(Hθ' := In_open_boxes _ _ Hin0).
+             repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union.
+              simpl. rewrite union_difference_L by trivial. ms.
+         -- intro HF. apply (Hnin _ Hin0). simpl. tauto.
+      * erewrite E_irr with (ϕ' := ψ).
+          exch 0. apply IHHp2. occ. rewrite Heq'. (* TODO: equiv_tac should do that *) equiv_tac.
+- split; Etac.
+  + foldEA. apply ImpBox.
+        -- do 2 apply weakening. apply ImpR.
+            erewrite E_irr with (ϕ' := φ1) by ms.
+            apply IHHp1.
+            ++ intros φ0 Hin1 HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ).
+                    apply (Hnin θ0); ms.
+            ++ rewrite Heq'.
+                    repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union.
+                    simpl. rewrite union_difference_R by auto with proof. ms.
+        -- apply IHHp2. occ. equiv_tac. trivial.
+  + foldEA. Atac. apply AndR.
+     * apply ImpBox.
+        -- do 2 apply weakening. apply ImpR.
+            erewrite E_irr with (ϕ' := φ1).
+            apply IHHp1.
+            ++ intros φ0 Hin1 HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ).
+                    apply (Hnin θ0); ms.
+            ++ rewrite Heq', union_difference_R, open_boxes_disj_union, open_boxes_remove by trivial. ms.
+       -- apply BoxR. box_tac. do 2 apply weakening. apply ImpR. foldEA.
+           erewrite E_irr with (ϕ' := φ1) by ms.
+           apply IHHp1.
+            ++ intros φ0 Hin1 HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ).
+                    apply (Hnin θ0); ms.
+            ++ rewrite Heq', union_difference_R, open_boxes_disj_union, open_boxes_remove by trivial. ms.
+     * foldEA. apply ImpBox.
+        ++ do 2 apply weakening. apply ImpR.
+               erewrite E_irr with (ϕ' := φ1).
+               apply IHHp1.
+               ** intros φ0 Hφ0 HF. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ).
+                     apply (Hnin θ0); ms.
+               ** rewrite Heq'.
+                     repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union.
+                     simpl. rewrite union_difference_R. ms. auto with proof.
+        ++ apply IHHp2; [occ|equiv_tac].
+- split.
+  + intro Hocc. destruct (open_boxes_case Δ) as [[θ Hθ] | Hequiv].
+      * Etac. foldEA. apply BoxR. box_tac. exch 0.
+        erewrite E_irr with (ϕ' := φ); apply IHHp.
+        -- intros φ0 Hφ0 HF. apply gmultiset_elem_of_disj_union in Hφ0.
+            destruct Hφ0 as [Hφ0|]; [|ms].
+            destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms.
+        -- rewrite Heq.
+            repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union.
+            simpl. auto with proof. rewrite <- difference_singleton by auto with proof. ms.
+        -- trivial.
+      * apply BoxR. box_tac. exch 0. apply open_box_L.
+         erewrite E_irr with (ϕ' := φ).
+         apply IHHp.
+         -- intros φ0 Hφ0 HF. apply gmultiset_elem_of_disj_union in Hφ0.
+            destruct Hφ0 as [Hφ0|]; [|ms].
+            destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms.
+         -- rewrite Hequiv, Heq. rewrite open_boxes_disj_union. ms.
+         -- trivial.
+  + Atac'. foldEA. apply BoxR. box_tac. apply weakening. erewrite E_irr with (ϕ' := φ).
+       apply weakening. apply make_impl_sound_R, ImpR.
+       apply IHHp.
+       * intros φ0 Hφ0 HF. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ).
+          apply (Hnin θ0); ms.
+       * rewrite Heq, open_boxes_disj_union. ms.
+Qed.
+ +
+End PropQuantCorrect.
+ +
+End Correctness.
+ +
+End Pitts.
+ +
+
+ +
+

Pitts' Theorem

+ +
+
+ +
+Open Scope type_scope.
+ +
+Lemma E_of_empty p φ : E p (∅, φ) = (Implies Bot Bot).
+Proof.
+  rewrite E_eq. rewrite in_map_empty. now unfold conjunction, nodup, foldl.
+Qed.
+ +
+Definition vars_incl φ l := forall x, occurs_in x φ -> In x l.
+ +
+
+ +
+ The overall correctness result is summarized here. +
+
+ +
+Theorem pitts p V: p ∉ V ->
+  ∀ φ, vars_incl φ (p :: V) ->
+    (vars_incl (Ef p φ) V)
+  * ({[φ]} ⊢ (Ef p φ))
+  * (∀ ψ, vars_incl ψ V -> {[φ]} ⊢ ψ -> {[Ef p φ]} ⊢ ψ)
+  * (vars_incl (Af p φ) V)
+  * ({[Af p φ]} ⊢ φ)
+  * (∀ θ, vars_incl θ V -> {[θ]} ⊢ φ -> {[θ]} ⊢ Af p φ).
+Proof.
+intros Hp φ Hvarsφ; repeat split.
+ +
+  + intros x Hx. apply (EA_vars p _ ⊥ x) in Hx.
+      destruct Hx as [Hneq [θ [Hθ Hocc]]]. apply gmultiset_elem_of_singleton in Hθ. subst.
+      apply Hvarsφ in Hocc. destruct Hocc; subst; tauto.
+  + apply entail_correct.
+  + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp. unfold Ef. rewrite E_irr with (ϕ' := ψ).
+      * peapply (pq_correct p ∅ {[φ]} ψ).
+         -- intros θ Hin. inversion Hin.
+         -- peapply Hyp.
+         -- intro HF. apply Hψ in HF. tauto.
+  + intros x Hx. apply (EA_vars p ∅ φ x) in Hx.
+      destruct Hx as [Hneq [Hin | [θ [Hθ Hocc]]]].
+      * apply Hvarsφ in Hin. destruct Hin; subst; tauto.
+      * inversion Hθ.
+  + peapply (entail_correct p ∅).
+  + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp.
+      apply (TopL_rev _ ⊥). peapply (pq_correct p {[ψ]} ∅ φ).
+      * intros φ0 Hφ0. apply gmultiset_elem_of_singleton in Hφ0. subst. auto with *.
+      * peapply Hyp.
+      * now rewrite E_of_empty.
+Qed.
+ +
+
+
+ +
+ + + diff --git a/html/ISL.SequentProps.html b/html/ISL.SequentProps.html new file mode 100644 index 0000000..9e40c2d --- /dev/null +++ b/html/ISL.SequentProps.html @@ -0,0 +1,1336 @@ + + + + + + + + + + + + + +
+
+

ISL.SequentProps

+ +
+Require Import ISL.Sequents.
+ +
+(* Required for dependent induction. *)
+Require Import Coq.Program.Equality.
+ +
+
+ +
+

Overview: admissible rules in G4ip sequent calculus

+ + +
+ +This file contains important properties of the sequent calculus G4ip, defined in +Sequents.v, namely the admissibility of various inversion rules, weakening and +contraction. We draw various consequences from this that are used extensively in +the proof of correctness of propositional quantifiers. The first part of this +file closely follows proof in the paper: + +
+ +(Dyckhoff and Negri 2000). R. Dyckhoff and S. Negri, Admissibility of Structural +Rules for Contraction-Free Systems of Intuitionistic Logic, Journal of Symbolic +Logic (65):4. + +
+ +

Weakening

+ +
+ + We prove the admissibility of the weakening rule. +
+
+ +
+Theorem weakening φ' Γ φ : Γ ⊢ φ -> Γ•φ' ⊢ φ.
+Proof with (auto with proof).
+intro H. revert φ'. induction H; intro φ'; auto with proof; try (exch 0; auto with proof).
+- constructor 4. exch 1; exch 0...
+- constructor 7; exch 0...
+- constructor 8; exch 0...
+- exch 1; constructor 9; exch 1; exch 0...
+- constructor 10; exch 0...
+- constructor 11. exch 1; exch 0...
+- constructor 12; exch 0...
+- apply ImpBox; box_tac.
+  + peapply (IHProvable1 (open_box φ')).
+  + exch 0...
+- apply BoxR. box_tac; exch 0...
+Qed.
+ +
+Global Hint Resolve weakening : proof.
+ +
+Theorem generalised_weakeningL (Γ Γ' : env) φ: Γ ⊢ φ -> Γ' ⊎ Γ ⊢ φ.
+Proof.
+intro Hp.
+induction Γ' as [| x Γ' IHΓ'] using gmultiset_rec.
+- peapply Hp.
+- peapply (weakening x). exact IHΓ'. ms.
+Qed.
+ +
+Theorem generalised_weakeningR (Γ Γ' : env) φ: Γ' ⊢ φ -> Γ' ⊎ Γ ⊢ φ.
+Proof.
+intro Hp.
+induction Γ as [| x Γ IHΓ] using gmultiset_rec.
+- peapply Hp.
+- peapply (weakening x). exact IHΓ. ms.
+Qed.
+ +
+Global Hint Extern 5 (?a <= ?b) => simpl in *; lia : proof.
+ +
+
+ +
+

Inversion rules

+ +
+ + We prove that the following rules are invertible: implication right, and + left, or left, top left (i.e., the appliction of weakening for the formula + top), the four implication left rules, the and right rule and the application of the or right rule with bottom. +
+
+ +
+Lemma ImpR_rev Γ φ ψ :
+  (Γ ⊢ (φ → ψ))
+    -> Γ•φ ⊢ ψ.
+Proof with (auto with proof).
+intro Hp. dependent induction Hp; auto with proof; try exch 0.
+- constructor 4. exch 1; exch 0...
+- constructor 7; exch 0...
+- exch 1; constructor 9; exch 1; exch 0...
+- constructor 10; exch 0...
+- constructor 11. exch 1; exch 0...
+- constructor 12; exch 0...
+- constructor 13; box_tac...
+  + exch 1; exch 0...
+  + exch 0. auto with proof.
+Qed.
+ +
+Global Hint Resolve ImpR_rev : proof.
+ +
+Theorem generalised_axiom Γ φ : Γ•φ ⊢ φ.
+Proof with (auto with proof).
+remember (weight φ) as w.
+assert(Hle : weight φ ≤ w) by lia.
+clear Heqw. revert Γ φ Hle.
+induction w; intros Γ φ Hle.
+- assert (Hφ := weight_pos φ). lia.
+- destruct φ; simpl in Hle...
+  destruct φ1 as [v| | θ1 θ2 | θ1 θ2 | θ1 θ2 | θ].
+  + constructor 8. exch 0...
+  + auto with proof.
+  + apply ImpR, AndL. exch 1; exch 0. apply ImpLAnd.
+    exch 0. apply ImpR_rev. exch 0...
+  + apply ImpR. exch 0. apply ImpLOr.
+    exch 1; exch 0...
+  + apply ImpR. exch 0...
+  + apply ImpR. exch 0. apply ImpBox; box_tac...
+  + apply BoxR; box_tac...
+Qed.
+ +
+Global Hint Resolve generalised_axiom : proof.
+ +
+Lemma open_box_L Γ φ ψ : Γ • φ ⊢ ψ -> Γ • ⊙ φ ⊢ ψ.
+Proof.
+intro Hp.
+remember (Γ•φ) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ φ ]}) by ms.
+assert(Hin : φ ∈ Γ')by ms.
+rw Heq 1. clear Γ HH Heq. revert φ Hin.
+dependent induction Hp generalizing Γ' Hp; intros φ0 Hin.
+- case (decide (φ0 = Var p)).
+  + intro; subst. simpl. auto with proof.
+  + intro. forward. auto with proof.
+- case (decide (φ0 = ⊥)).
+  + intro; subst. simpl. auto with proof.
+  + intro. forward. auto with proof.
+- apply AndR; auto.
+- case (decide (φ0 = (φ ∧ ψ))).
+  + intro; subst. simpl. apply AndL. peapply Hp.
+  + intro. forward. apply AndL. do 2 backward. peapply (IHHp φ0). ms.
+- apply OrR1; auto.
+- apply OrR2; auto.
+- case (decide (φ0 = (φ ∨ ψ))).
+  + intro; subst. simpl. apply OrL.
+      * peapply Hp1.
+      * peapply Hp2.
+  + intro. forward. apply OrL.
+      * backward. peapply (IHHp1 φ0). ms.
+      * backward. peapply (IHHp2 φ0). ms.
+- apply ImpR. backward. apply IHHp. ms.
+- case (decide (φ0 = Var p)).
+  + intro; subst; simpl. forward. apply ImpLVar. peapply Hp.
+  + intro. case (decide (φ0 = (Var p → φ))).
+      * intro; subst; simpl. peapply ImpLVar. exact Hp. ms.
+      * intro. do 2 forward. exch 0. apply ImpLVar. exch 0. do 2 backward.
+         apply IHHp. ms.
+- case (decide (φ0 = (φ1 ∧ φ2 → φ3))).
+  + intro; subst; simpl. apply ImpLAnd. peapply Hp.
+  + intro. forward. apply ImpLAnd. backward. apply IHHp. ms.
+- case (decide (φ0 = (φ1 ∨ φ2 → φ3))).
+  + intro; subst; simpl. apply ImpLOr. peapply Hp.
+  + intro. forward. apply ImpLOr. exch 0. do 2 backward. apply IHHp. ms.
+- case (decide (φ0 = ((φ1 → φ2) → φ3))).
+  + intro; subst; simpl. apply ImpLImp. peapply Hp1. peapply Hp2.
+  + intro. forward. apply ImpLImp.
+      * backward. apply IHHp1. ms.
+      * backward. apply IHHp2. ms.
+- case (decide (φ0 = (□ φ1 → φ2))).
+  + intro; subst; simpl. apply ImpBox.
+      * peapply Hp1; autorewrite with proof; ms.
+      * peapply Hp2; autorewrite with proof.
+  + intro. forward.
+      case (decide (open_box φ0 = □ φ1)).
+      * intro Heq. repeat rewrite Heq. apply ImpBox; box_tac.
+        -- exch 1; exch 0. apply generalised_axiom.
+        -- backward. rewrite <- Heq. apply IHHp2. auto with *.
+      * intro Hneq. case (decide (open_box φ0 = φ2)).
+          -- intro Heq. subst φ2. apply ImpBox; box_tac.
+              ++ peapply (IHHp1 (⊙ φ0)); [ms|].
+                      autorewrite with proof; [|ms]. repeat rewrite env_replace.
+                     ** ms.
+                     ** auto with proof.
+                     ** apply env_in_add. right. auto with proof; ms.
+              ++ box_tac. backward. apply (IHHp2 φ0). auto with *.
+          -- intro Hneq'. apply ImpBox; repeat box_tac.
+            ++ exch 0. box_tac. backward. backward. apply (IHHp1 (⊙ φ0)).
+                    apply env_in_add. now right.
+            ++ backward. apply IHHp2. apply env_in_add. now right.
+- case (decide (open_box φ0 = □ φ)).
+  + intro Heq; rewrite Heq. apply generalised_axiom.
+  + intro. backward. apply BoxR. box_tac.
+      case (decide (open_box φ0 = open_box (open_box φ0))).
+      * intro Heq. peapply Hp. autorewrite with proof. rewrite <- Heq. ms. ms.
+      * intro. assert( open_box φ0 ∈ open_boxes Γ) by (now apply In_open_boxes).
+        peapply (IHHp (open_box φ0)).
+        -- ms.
+        -- autorewrite with proof. repeat rewrite env_replace; ms. ms.
+Qed.
+ +
+Local Hint Resolve env_in_add : proof.
+ +
+Lemma AndL_rev Γ φ ψ θ: (Γ•φ ∧ ψ) ⊢ θ → (Γ•φ•ψ) ⊢ θ.
+Proof.
+intro Hp.
+remember (Γ•φ ∧ ψ) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ φ ∧ ψ ]}) by ms.
+assert(Hin : (φ ∧ ψ) ∈ Γ')by ms.
+rw Heq 2. clear Γ HH Heq. revert φ ψ Hin.
+(* we massaged the goal so that the environment of the derivation on which we do
+   the induction is not composite anymore *)
+induction Hp; intros φ0 ψ0 Hin; try forward.
+(* auto takes care of the right rules easily *)
+- auto with proof.
+- auto with proof.
+- auto with proof.
+(* the main case *)
+- case(decide ((φ ∧ ψ) = (φ0 ∧ ψ0))); intro Heq0.
+  + inversion Heq0; subst. peapply Hp.
+  + forward. constructor 4. exch 0. backward. backward. apply IHHp. ms.
+(* only left rules remain. Now it's all a matter of putting the right principal
+   formula at the front, apply the rule; and put back the front formula at the back
+   before applying the induction hypothesis *)
+- auto with proof.
+- auto with proof.
+- constructor 7; backward; [apply IHHp1 | apply IHHp2]; ms.
+- constructor 8. backward. apply IHHp. ms.
+- forward. exch 0. constructor 9. exch 0. do 2 backward. apply IHHp. ms.
+- constructor 10. backward. apply IHHp. ms.
+- constructor 11. exch 0. do 2 backward. apply IHHp. ms.
+- constructor 12; backward.
+  + apply IHHp1. ms.
+  + apply IHHp2. ms.
+- constructor 13; repeat box_tac.
+  + exch 0. box_tac.
+      apply In_open_boxes in Hin0. backward. backward. apply open_box_L. exch 0. apply open_box_L. exch 0.
+      apply IHHp1. ms.
+  + backward. apply IHHp2. ms.
+- constructor 14. repeat box_tac.
+  exch 0. apply open_box_L.
+  exch 1; exch 0. apply open_box_L.
+  peapply (IHHp φ0 ψ0).
+  + apply env_in_add. right. apply In_open_boxes in Hin. auto with proof.
+  + autorewrite with proof. simpl. rewrite <- env_replace. ms.
+      apply In_open_boxes in Hin. auto with proof.
+Qed.
+ +
+Lemma OrL_rev Γ φ ψ θ: (Γ•φ ∨ ψ) ⊢ θ → (Γ•φ ⊢ θ) * (Γ•ψ ⊢ θ).
+Proof.
+intro Hp.
+remember (Γ•φ ∨ ψ) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ φ ∨ ψ ]}) by ms.
+assert(Hin : (φ ∨ ψ) ∈ Γ')by ms.
+assert(Heq' : ((Γ' ∖ {[φ ∨ ψ]}•φ) ⊢ θ) * ((Γ' ∖ {[φ ∨ ψ]}•ψ) ⊢ θ));
+[| split; rw Heq 1; tauto].
+clear Γ HH Heq.
+induction Hp.
+- split; forward; auto with proof.
+- split; forward; auto with proof.
+- split; constructor 3; intuition.
+- split; forward; constructor 4; exch 0; do 2 backward; apply IHHp; ms.
+- split; constructor 5; intuition.
+- split; apply OrR2; intuition.
+- case (decide ((φ0 ∨ ψ0) = (φ ∨ ψ))); intro Heq0.
+  + inversion Heq0; subst. split; [peapply Hp1| peapply Hp2].
+  + split; forward; constructor 7; backward; (apply IHHp1||apply IHHp2); ms.
+- split; constructor 8; backward; apply IHHp; ms.
+- split; do 2 forward; exch 0; constructor 9; exch 0; do 2 backward; apply IHHp; ms.
+- split; forward; constructor 10; backward; apply IHHp; ms.
+- split; forward; constructor 11; exch 0; do 2 backward; apply IHHp; ms.
+- split; forward; constructor 12; backward; (apply IHHp1 || apply IHHp2); ms.
+- split; forward; assert(Hin' : (φ ∨ ψ) ∈ (⊗ Γ • □ φ1 • φ2))
+  by (apply env_in_add; right; apply env_in_add; right; auto with proof);
+  assert((φ ∨ ψ) ∈ ⊗Γ) by auto with proof;
+  (constructor 13; repeat box_tac; exch 0;
+    [do 2 backward; apply open_box_L; apply IHHp1|exch 0; backward; apply IHHp2];ms).
+- assert (Hin' : (φ ∨ ψ) ∈ (⊗ Γ • □ φ0)) by (apply env_in_add; right; auto with proof).
+    split; constructor 14; repeat box_tac; backward; apply open_box_L; now apply IHHp.
+Qed.
+ +
+Lemma TopL_rev Γ φ θ: Γ•(⊥ → φ) ⊢ θ -> Γ ⊢ θ.
+Proof.
+remember (Γ•(⊥ → φ)) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ ⊥ → φ ]}) by ms.
+assert(Hin : (⊥ → φ) ∈ Γ')by ms. clear HH.
+intro Hp. rw Heq 0. clear Γ Heq. induction Hp;
+try forward.
+- auto with proof.
+- auto with proof.
+- auto with proof.
+- constructor 4. exch 0. do 2 backward. apply IHHp. ms.
+- auto with proof.
+- auto with proof.
+- constructor 7; backward; [apply IHHp1 | apply IHHp2]; ms.
+- constructor 8. backward. apply IHHp. ms.
+- forward. exch 0. constructor 9. exch 0. do 2 backward. apply IHHp. ms.
+- constructor 10. backward. apply IHHp. ms.
+- constructor 11. exch 0. do 2 backward. apply IHHp. ms.
+- constructor 12; backward; [apply IHHp1 | apply IHHp2]; ms.
+- constructor 13; box_tac.
+  + exch 0. do 2 backward. apply IHHp1. ms.
+  + backward. apply IHHp2. ms.
+- constructor 14. box_tac. backward. apply IHHp. ms.
+Qed.
+ +
+Local Hint Immediate TopL_rev : proof.
+ +
+Lemma ImpLVar_rev Γ p φ ψ: (Γ•Var p•(p → φ)) ⊢ ψ → (Γ•Var p•φ) ⊢ ψ.
+Proof.
+intro Hp.
+remember (Γ•Var p•(p → φ)) as Γ' eqn:HH.
+assert (Heq: (Γ•Var p) ≡ Γ' ∖ {[Var p → φ]}) by ms.
+assert(Hin : (p → φ) ∈ Γ')by ms.
+rw Heq 1. clear Γ HH Heq.
+induction Hp; try forward.
+- auto with proof.
+- auto with proof.
+- auto with proof.
+- apply AndL. exch 0. do 2 backward. apply IHHp. ms.
+- auto with proof.
+- auto with proof.
+- apply OrL; backward; apply IHHp1 || apply IHHp2; ms.
+- apply ImpR. backward. apply IHHp. ms.
+- case (decide ((Var p0 → φ0) = (Var p → φ))); intro Heq0.
+  + inversion Heq0; subst. peapply Hp.
+  + do 2 forward. exch 0. apply ImpLVar. exch 0; do 2 backward. apply IHHp. ms.
+- apply ImpLAnd. backward. apply IHHp. ms.
+- apply ImpLOr. exch 0; do 2 backward. apply IHHp. ms.
+- apply ImpLImp; backward; (apply IHHp1 || apply IHHp2); ms.
+- apply ImpBox; repeat box_tac.
+   + exch 0; do 2 backward. apply open_box_L. apply IHHp1. ms.
+   + backward. apply IHHp2. ms.
+- apply BoxR. repeat box_tac. backward. apply open_box_L. apply IHHp. ms.
+Qed.
+ +
+(* inversion for ImpLImp is only partial *)
+Lemma ImpLImp_prev Γ φ1 φ2 φ3 ψ: (Γ•((φ1 → φ2) → φ3)) ⊢ ψ -> (Γ•φ3) ⊢ ψ.
+Proof.
+intro Hp.
+remember (Γ •((φ1 → φ2) → φ3)) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ ((φ1 → φ2) → φ3) ]}) by ms.
+assert(Hin :((φ1 → φ2) → φ3) ∈ Γ')by ms.
+rw Heq 1. clear Γ HH Heq.
+induction Hp; try forward.
+- auto with proof.
+- auto with proof.
+- auto with proof.
+- apply AndL. exch 0; do 2 backward. apply IHHp. ms.
+- auto with proof.
+- auto with proof.
+- apply OrL; backward; [apply IHHp1 | apply IHHp2]; ms.
+- apply ImpR. backward. apply IHHp. ms.
+- forward. exch 0. apply ImpLVar. exch 0. do 2 backward. apply IHHp. ms.
+- apply ImpLAnd. backward. apply IHHp. ms.
+- apply ImpLOr. exch 0. do 2 backward. apply IHHp. ms.
+- case (decide (((φ0 → φ4) → φ5) = ((φ1 → φ2) → φ3))); intro Heq0.
+  + inversion Heq0; subst. peapply Hp2.
+  + forward. apply ImpLImp; backward; (apply IHHp1 || apply IHHp2); ms.
+- apply ImpBox; repeat box_tac.
+  + exch 0; do 2 backward. apply open_box_L. apply IHHp1. ms.
+  + backward. apply IHHp2. ms.
+- apply BoxR. repeat box_tac. backward. apply open_box_L. apply IHHp. ms.
+Qed.
+ +
+(* inversion for ImpLbox is only partial too *)
+Lemma ImpLBox_prev Γ φ1 φ2 ψ: (Γ•((□φ1) → φ2)) ⊢ ψ -> (Γ•φ2) ⊢ ψ.
+Proof.
+intro Hp.
+remember (Γ •((□φ1) → φ2)) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ ((□φ1) → φ2) ]}) by ms.
+assert(Hin :((□φ1) → φ2) ∈ Γ')by ms.
+rw Heq 1. clear Γ HH Heq.
+induction Hp; try forward.
+- auto with proof.
+- auto with proof.
+- auto with proof.
+- apply AndL. exch 0; do 2 backward. apply IHHp. ms.
+- auto with proof.
+- auto with proof.
+- apply OrL; backward; [apply IHHp1 | apply IHHp2]; ms.
+- apply ImpR. backward. apply IHHp. ms.
+- forward. exch 0. apply ImpLVar. exch 0. do 2 backward. apply IHHp. ms.
+- apply ImpLAnd. backward. apply IHHp. ms.
+- apply ImpLOr. exch 0. do 2 backward. apply IHHp. ms.
+- apply ImpLImp; backward; (apply IHHp1 || apply IHHp2); ms.
+- case (decide((□φ0 → φ3) = (□φ1 → φ2))).
+  + intro Heq; inversion Heq; subst. peapply Hp2.
+  + intro Hneq. forward. apply ImpBox; repeat box_tac.
+     * exch 0; do 2 backward. apply open_box_L; apply IHHp1. ms.
+     * backward. apply IHHp2. ms.
+- apply BoxR. repeat box_tac. backward. apply open_box_L. apply IHHp. ms.
+Qed.
+ +
+Lemma ImpLOr_rev Γ φ1 φ2 φ3 ψ: Γ•((φ1 ∨ φ2) → φ3) ⊢ ψ -> Γ•(φ1 → φ3)•(φ2 → φ3) ⊢ ψ.
+Proof.
+intro Hp.
+remember (Γ •((φ1 ∨ φ2) → φ3)) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ ((φ1 ∨ φ2) → φ3) ]}) by ms.
+assert(Hin :((φ1 ∨ φ2) → φ3) ∈ Γ')by ms.
+rw Heq 2. clear Γ HH Heq.
+induction Hp; try forward.
+- auto with proof.
+- auto with proof.
+- auto with proof.
+- constructor 4. exch 0; do 2 backward. apply IHHp. ms.
+- auto with proof.
+- auto with proof.
+- constructor 7; backward; [apply IHHp1 | apply IHHp2]; ms.
+- constructor 8. backward. apply IHHp. ms.
+- forward. exch 0. constructor 9. exch 0. do 2 backward. apply IHHp. ms.
+- constructor 10. backward. apply IHHp. ms.
+- case (decide (((φ0 ∨ φ4) → φ5) = ((φ1 ∨ φ2) → φ3))); intro Heq0.
+  + inversion Heq0; subst. peapply Hp.
+  + forward. constructor 11; exch 0; do 2 backward; apply IHHp; ms.
+- constructor 12; backward; (apply IHHp1 || apply IHHp2); ms.
+- apply ImpBox; repeat box_tac.
+  + exch 0; do 2 backward. apply IHHp1. ms.
+  + backward. apply IHHp2. ms.
+- apply BoxR. repeat box_tac. backward. apply IHHp. ms.
+Qed.
+ +
+Lemma ImpLAnd_rev Γ φ1 φ2 φ3 ψ: (Γ•(φ1 ∧ φ2 → φ3)) ⊢ ψ -> (Γ•(φ1 → φ2 → φ3)) ⊢ ψ .
+Proof.
+intro Hp.
+remember (Γ •((φ1 ∧ φ2) → φ3)) as Γ' eqn:HH.
+assert (Heq: Γ ≡ Γ' ∖ {[ ((φ1 ∧ φ2) → φ3) ]}) by ms.
+assert(Hin :((φ1 ∧ φ2) → φ3) ∈ Γ')by ms.
+rw Heq 1. clear Γ HH Heq.
+induction Hp; try forward.
+- auto with proof.
+- auto with proof.
+- auto with proof.
+- constructor 4. exch 0; do 2 backward. apply IHHp. ms.
+- auto with proof.
+- auto with proof.
+- constructor 7; backward; [apply IHHp1 | apply IHHp2]; ms.
+- constructor 8. backward. apply IHHp. ms.
+- forward. exch 0. constructor 9. exch 0. do 2 backward. apply IHHp. ms.
+- case (decide (((φ0 ∧ φ4) → φ5) = ((φ1 ∧ φ2) → φ3))); intro Heq0.
+  + inversion Heq0; subst. peapply Hp.
+  + forward. constructor 10. backward. apply IHHp. ms.
+- constructor 11; exch 0; do 2 backward; apply IHHp; ms.
+- constructor 12; backward; (apply IHHp1 || apply IHHp2); ms.
+- apply ImpBox; repeat box_tac.
+  + exch 0; do 2 backward. apply IHHp1. ms.
+  + backward. apply IHHp2. ms.
+- apply BoxR. repeat box_tac. backward. apply IHHp. ms.
+Qed.
+ +
+Global Hint Resolve AndL_rev : proof.
+Global Hint Resolve OrL_rev : proof.
+Global Hint Resolve ImpLVar_rev : proof.
+Global Hint Resolve ImpLOr_rev : proof.
+Global Hint Resolve ImpLAnd_rev : proof.
+Global Hint Resolve ImpLBox_prev : proof.
+ +
+Lemma exfalso Γ φ: Γ ⊢ ⊥ -> Γ ⊢ φ.
+Proof.
+intro Hp. dependent induction Hp; try tauto; auto with proof; tauto.
+Qed.
+ +
+Global Hint Immediate exfalso : proof.
+ +
+Lemma AndR_rev {Γ φ1 φ2} : Γ ⊢ φ1 ∧ φ2 -> (Γ ⊢ φ1) * (Γ ⊢ φ2).
+Proof. intro Hp. dependent induction Hp generalizing φ1 φ2 Hp; intuition; auto with proof. Qed.
+ +
+
+ +
+A general inversion rule for disjunction is not admissible. However, inversion holds if one of the formulas is ⊥. +
+
+ +
+Lemma OrR1Bot_rev Γ φ : Γ ⊢ φ ∨ ⊥ -> Γ ⊢ φ.
+Proof. intro Hd. dependent induction Hd; auto with proof. Qed.
+Lemma OrR2Bot_rev Γ φ : Γ ⊢ ⊥ ∨ φ -> Γ ⊢ φ.
+Proof. intro Hd. dependent induction Hd; auto with proof. Qed.
+ +
+
+ +
+We prove Lemma 4.1 of (Dyckhoff & Negri 2000). This lemma shows that a + weaker version of the ImpL rule of Gentzen's original calculus LJ is still + admissible in G4ip. The proof is simple, but requires the inversion lemmas + proved above. + +
+
+ +
+Lemma weak_ImpL Γ φ ψ θ :Γ ⊢ φ -> Γ•ψ ⊢ θ -> Γ•(φ → ψ) ⊢ θ.
+Proof with (auto with proof).
+intro Hp. revert ψ θ. induction Hp; intros ψ0 θ0 Hp'.
+- auto with proof.
+- auto with proof.
+- auto with proof.
+- exch 0; constructor 4; exch 1; exch 0...
+- auto with proof.
+- apply ImpLOr. exch 0...
+- exch 0; constructor 7; exch 0...
+  + apply IHHp1. exch 0. eapply fst, OrL_rev. exch 0. exact Hp'.
+  + apply IHHp2. exch 0. eapply snd, OrL_rev. exch 0. exact Hp'.
+- auto with proof.
+- exch 0; exch 1. constructor 9. exch 1; exch 0...
+- exch 0. apply ImpLAnd. exch 0...
+- exch 0. apply ImpLOr. exch 1; exch 0...
+- exch 0. apply ImpLImp; exch 0... apply IHHp2. exch 0...
+  eapply ImpLImp_prev. exch 0. eassumption.
+- exch 0. apply ImpBox; box_tac.
+  + exch 1; exch 0...
+  + exch 0. apply IHHp2. exch 0. apply ImpLBox_prev with φ1. exch 0. exact Hp'.
+- auto with proof.
+Qed.
+ +
+Global Hint Resolve weak_ImpL : proof.
+ +
+
+ +
+

Contraction

+ + +
+ + The aim of this section is to prove that the contraction rule is admissible in + G4ip. +
+ + An auxiliary definition of **height** of a proof, measured along the leftmost branch. +
+
+Fixpoint height {Γ φ} (Hp : Γ ⊢ φ) := match Hp with
+| Atom _ _ => 1
+| ExFalso _ _ => 1
+| AndR Γ φ ψ H1 H2 => 1 + height H1 + height H2
+| AndL Γ φ ψ θ H => 1 + height H
+| OrR1 Γ φ ψ H => 1 + height H
+| OrR2 Γ φ ψ H => 1 + height H
+| OrL Γ φ ψ θ H1 H2 => 1 + height H1 + height H2
+| ImpR Γ φ ψ H => 1 + height H
+| ImpLVar Γ p φ ψ H => 1 + height H
+| ImpLAnd Γ φ1 φ2 φ3 ψ H => 1 + height H
+| ImpLOr Γ φ1 φ2 φ3 ψ H => 1 + height H
+| ImpLImp Γ φ1 φ2 φ3 ψ H1 H2 => 1 + height H1 + height H2
+| ImpBox Γ φ1 φ2 ψ H1 H2 => 1 + height H1 + height H2
+| BoxR Γ φ H => 1 + height H
+end.
+ +
+Lemma height_0 {Γ φ} (Hp : Γ ⊢ φ) : height Hp <> 0.
+Proof. destruct Hp; simpl; lia. Qed.
+ +
+
+ +
+Lemma 4.2 in (Dyckhoff & Negri 2000), showing that a "duplication" in the context of the implication-case of the implication-left rule is admissible. +
+
+ +
+Lemma ImpLImp_dup Γ φ1 φ2 φ3 θ:
+  Γ•((φ1 → φ2) → φ3) ⊢ θ ->
+    Γ•φ1 •(φ2 → φ3) •(φ2 → φ3) ⊢ θ.
+Proof.
+intro Hp.
+remember (Γ•((φ1 → φ2) → φ3)) as Γ0 eqn:Heq0.
+assert(HeqΓ : Γ ≡ Γ0 ∖ {[((φ1 → φ2) → φ3)]}) by ms.
+rw HeqΓ 3.
+assert(Hin : ((φ1 → φ2) → φ3) ∈ Γ0) by (subst Γ0; ms).
+clear Γ HeqΓ Heq0.
+(* by induction on the height of the derivation *)
+remember (height Hp) as h.
+assert(Hleh : height Hp ≤ h) by lia. clear Heqh.
+revert Γ0 θ Hp Hleh Hin. induction h as [|h]; intros Γ θ Hp Hleh Hin;
+[pose (height_0 Hp); lia|].
+destruct Hp; simpl in Hleh.
+- forward. auto with proof.
+- forward. auto with proof.
+- apply AndR.
+  + apply IHh with Hp1. lia. ms.
+  + apply IHh with Hp2. lia. ms.
+- forward. apply AndL. exch 0. do 2 backward. apply IHh with Hp. lia. ms.
+- apply OrR1. apply IHh with Hp. lia. ms.
+- apply OrR2. apply IHh with Hp. lia. ms.
+- forward. apply OrL; backward.
+  + apply IHh with Hp1. lia. ms.
+  + apply IHh with Hp2. lia. ms.
+- apply ImpR. backward. apply IHh with Hp. lia. ms.
+- do 2 forward. exch 0. apply ImpLVar. exch 0. do 2 backward.
+  apply IHh with Hp. lia. ms.
+- forward. apply ImpLAnd. backward. apply IHh with Hp. lia. ms.
+- forward. apply ImpLOr. exch 0. do 2 backward. apply IHh with Hp. lia. ms.
+- case (decide (((φ0 → φ4) → φ5) = ((φ1 → φ2) → φ3))); intro Heq.
+  + inversion Heq; subst.
+    apply weak_ImpL.
+    * exch 0. apply ImpR_rev. peapply Hp1.
+    * do 2 (exch 0; apply weakening). peapply Hp2.
+  + forward. apply ImpLImp; backward.
+    * apply IHh with Hp1. lia. ms.
+    * apply IHh with Hp2. lia. ms.
+- forward. apply ImpBox; repeat box_tac.
+  + exch 0. do 2 backward.
+      exch 1; exch 0. apply open_box_L; exch 0; exch 1.
+      apply IHh with Hp1. lia. ms.
+  + backward. apply IHh with Hp2. lia. ms.
+- apply BoxR. repeat box_tac. backward.
+  exch 1; exch 0; apply open_box_L; exch 0; exch 1.
+  apply IHh with Hp. lia. ms.
+Qed.
+ +
+Lemma ImpBox_dup Γ φ1 φ2 θ:
+  Γ•(□φ1 → φ2) ⊢ θ ->
+    Γ • □ φ1 • □ φ1 • φ2 ⊢ θ.
+Proof.
+intro Hp.
+remember (Γ• (□ φ1 → φ2)) as Γ0 eqn:Heq0.
+assert(HeqΓ : Γ ≡ Γ0 ∖ {[(□ φ1 → φ2)]}) by ms.
+rw HeqΓ 3.
+assert(Hin : (□ φ1 → φ2) ∈ Γ0) by (subst Γ0; ms).
+clear Γ HeqΓ Heq0.
+(* by induction on the height of the derivation *)
+remember (height Hp) as h.
+assert(Hleh : height Hp ≤ h) by lia. clear Heqh.
+revert Γ0 θ Hp Hleh Hin. induction h as [|h]; intros Γ θ Hp Hleh Hin;
+[pose (height_0 Hp); lia|].
+destruct Hp; simpl in Hleh.
+- forward. auto with proof.
+- forward. auto with proof.
+- apply AndR.
+  + apply IHh with Hp1. lia. ms.
+  + apply IHh with Hp2. lia. ms.
+- forward. apply AndL. exch 0. do 2 backward. apply IHh with Hp. lia. ms.
+- apply OrR1. apply IHh with Hp. lia. ms.
+- apply OrR2. apply IHh with Hp. lia. ms.
+- forward. apply OrL; backward.
+  + apply IHh with Hp1. lia. ms.
+  + apply IHh with Hp2. lia. ms.
+- apply ImpR. backward. apply IHh with Hp. lia. ms.
+- do 2 forward. exch 0. apply ImpLVar. exch 0. do 2 backward.
+  apply IHh with Hp. lia. ms.
+- forward. apply ImpLAnd. backward. apply IHh with Hp. lia. ms.
+- forward. apply ImpLOr. exch 0. do 2 backward. apply IHh with Hp. lia. ms.
+- forward. apply ImpLImp.
+  + backward. apply IHh with Hp1. lia. ms.
+  + backward. apply IHh with Hp2. lia. ms.
+  (*
+case (decide (((φ0 → φ4) → φ5) = ((φ1 → φ2) → φ3))); intro Heq.
+  + inversion Heq; subst.
+    apply weak_ImpL.
+    * exch 0. apply ImpR_rev. peapply Hp1.
+    * do 2 (exch 0; apply weakening). peapply Hp2.
+  + forward. apply ImpLImp; backward.
+    * apply IHh with Hp1. lia. ms.
+    * apply IHh with Hp2. lia. ms. *)
+- case (decide ((□ φ0 → φ3) = □ φ1 → φ2)); intro Heq.
+  + inversion Heq; subst.
+      exch 0. apply weakening. exch 0. apply weakening. peapply Hp2.
+  + forward. apply ImpBox; repeat box_tac.
+      * exch 0. do 2 backward.
+         replace (φ1) with (⊙ (□ φ1)) by trivial.
+         apply open_box_L; exch 0. apply open_box_L; exch 1; exch 0. apply open_box_L.
+         exch 1; exch 0. simpl.
+         apply IHh with Hp1. lia. ms.
+      * backward. apply IHh with Hp2. lia. ms.
+- apply BoxR. repeat box_tac. backward.
+   replace (φ1) with (⊙ (□ φ1)) by trivial.
+   apply open_box_L; exch 0. apply open_box_L; exch 1; exch 0. apply open_box_L.
+   exch 1; exch 0. simpl.
+  apply IHh with Hp. lia. ms.
+Qed.
+ +
+(* technical lemma for contraction *)
+Local Lemma p_contr Γ φ θ:
+  (Γ•φ•φ) ∖ {[φ]} ⊢ θ ->
+  ((Γ•φ) ⊢ θ).
+Proof. intros * Hd; peapply Hd. Qed.
+ +
+Lemma is_box_weight_open_box φ : is_box φ = true -> weight (⊙ φ) = weight φ -1.
+Proof. destruct φ; simpl; lia. Qed.
+ +
+Lemma weight_open_box φ : weight (⊙ φ) ≤ weight φ.
+Proof. destruct φ; simpl; lia. Qed.
+ +
+
+ +
+Admissibility of contraction in G4ip. +
+
+Lemma contraction Γ ψ θ : Γ•ψ•ψ ⊢ θ -> Γ•ψ ⊢ θ.
+Proof.
+remember (Γ•ψ•ψ) as Γ0 eqn:Heq0.
+assert(HeqΓ : (Γ•ψ) ≡ Γ0 ∖ {[ψ]}) by ms.
+intro Hp. rw HeqΓ 0.
+assert(Hin : ψ ∈ Γ0) by (subst Γ0; ms).
+assert(Hin' : ψ ∈ Γ0 ∖ {[ψ]}) by(rewrite <- HeqΓ; ms).
+clear Γ HeqΓ Heq0. revert Hp.
+(* by induction on the weight of ψ *)
+remember (weight ψ) as w.
+assert(Hle : weight ψ ≤ w) by lia.
+clear Heqw. revert Γ0 ψ θ Hle Hin Hin'.
+induction w; intros Γ ψ θ Hle Hin Hin' Hp; [destruct ψ; simpl in Hle; lia|].
+(* by induction on the height of the premise *)
+remember (height Hp) as h.
+assert(Hleh : height Hp ≤ h) by lia. clear Heqh.
+revert Γ θ Hp Hleh Hin Hin'. revert ψ Hle; induction h as [|h]; intros ψ Hle Γ θ Hp Hleh Hin Hin';
+[pose (height_0 Hp); lia|].
+destruct Hp; simpl in Hleh, Hle.
+- case(decide (ψ = Var p)).
+  + intro; subst. exhibit Hin' 0. apply Atom.
+  + intro Hneq. forward. apply Atom.
+- case(decide (ψ = ⊥)).
+  + intro; subst. exhibit Hin' 0. apply ExFalso.
+  + intro. forward. apply ExFalso.
+- apply AndR.
+  + apply (IHh ψ Hle) with Hp1. lia. ms. ms.
+  + apply (IHh ψ Hle) with Hp2. lia. ms. ms.
+- case (decide (ψ = (φ ∧ ψ0))); intro Heq.
+  + subst. exhibit Hin' 0. apply AndL.
+    apply p_contr. simpl in Hle. apply IHw. lia. ms. rewrite union_difference_R; ms.
+    exch 1. exch 0. apply p_contr. apply IHw. lia. ms. rewrite union_difference_R; ms.
+    exch 1. exch 0. apply AndL_rev. exch 0. exch 1. peapply Hp.
+    rewrite <- (difference_singleton _ _ Hin'). ms.
+  + rewrite union_difference_L in Hin' by ms.
+    forward. apply AndL. exch 0. do 2 backward. apply (IHh ψ Hle) with Hp. lia. ms. ms.
+- apply OrR1. apply (IHh ψ Hle) with Hp. lia. ms. ms.
+- apply OrR2. apply (IHh ψ Hle) with Hp. lia. ms. ms.
+- case (decide (ψ = (φ ∨ ψ0))); intro Heq.
+  + subst. exhibit Hin' 0.
+    apply OrL.
+    * apply p_contr. simpl in Hle. apply IHw. lia. ms. rewrite union_difference_R; ms.
+      refine (fst (OrL_rev _ φ ψ0 _ _)). exch 0. peapply Hp1.
+      rewrite <- env_replace; ms.
+    * apply p_contr. simpl in Hle. apply IHw. lia. ms. rewrite union_difference_R; ms.
+      refine (snd (OrL_rev _ φ ψ0 _ _)). exch 0. peapply Hp2.
+      rewrite <- env_replace; ms.
+  + rewrite union_difference_L in Hin' by ms.
+    forward. apply OrL; backward.
+    * apply (IHh ψ Hle) with Hp1. lia. ms. ms.
+    * apply (IHh ψ Hle) with Hp2. lia. ms. ms.
+- apply ImpR. backward. apply (IHh ψ Hle) with Hp. lia. ms. ms.
+- case (decide (ψ = (p → φ))); intro Heq.
+  + subst. exhibit Hin' 0. rewrite union_difference_R in Hin' by ms.
+    assert(Hcut : (((Γ•Var p) ∖ {[Var p → φ]}•(Var p → φ)) ⊢ ψ0)); [|peapply Hcut].
+    forward. exch 0. apply ImpLVar, p_contr.
+    apply IHw. simpl in Hle; lia. ms. rewrite union_difference_L; ms.
+    exch 1. apply ImpLVar_rev. exch 0; exch 1. peapply Hp.
+    rewrite <- env_replace; ms.
+  + rewrite union_difference_L in Hin' by ms.
+      forward. case (decide (ψ = Var p)).
+      * intro; subst. forward. exch 0. apply ImpLVar. exch 0.
+         do 2 backward. apply (IHh (Var p) Hle) with Hp. lia. ms. ms.
+      * intro. forward. exch 0. apply ImpLVar; exch 0; do 2 backward.
+         apply (IHh ψ Hle) with Hp. lia. ms. ms.
+- case (decide (ψ = (φ1 ∧ φ2 → φ3))); intro Heq.
+  + subst. exhibit Hin' 0. rewrite union_difference_R in Hin' by ms.
+    apply ImpLAnd. apply p_contr.
+    apply IHw. simpl in *; lia. ms. rewrite union_difference_L; ms.
+    apply ImpLAnd_rev. exch 0. peapply Hp.
+    rewrite <- env_replace; ms.
+  + rewrite union_difference_L in Hin' by ms.
+    forward. apply ImpLAnd. backward. apply (IHh ψ Hle) with Hp. lia. ms. ms.
+- case (decide (ψ = (φ1 ∨ φ2 → φ3))); intro Heq.
+  + subst. exhibit Hin' 0. rewrite union_difference_R in Hin' by ms.
+    apply ImpLOr. apply p_contr.
+    apply IHw. simpl in *; lia. ms. rewrite union_difference_L; ms.
+    exch 1; exch 0. apply p_contr.
+    apply IHw. simpl in *. lia. ms. rewrite union_difference_L; ms.
+    exch 1; exch 0. apply ImpLOr_rev. exch 0. exch 1. peapply Hp.
+    rewrite <- env_replace; ms.
+  + rewrite union_difference_L in Hin' by ms.
+    forward. apply ImpLOr. exch 0. do 2 backward. apply (IHh ψ Hle) with Hp. lia. ms. ms.
+- case (decide (ψ = ((φ1 → φ2) → φ3))); intro Heq.
+  + subst. exhibit Hin' 0. rewrite union_difference_R in Hin' by ms.
+    apply ImpLImp.
+    * apply ImpR.
+      do 3 (exch 0; apply p_contr; apply IHw; [simpl in *; lia|ms|rewrite union_difference_L; ms|exch 1]).
+      exch 1; apply ImpLImp_dup. (* key lemma *)
+      exch 0; exch 1. apply ImpR_rev.
+      peapply Hp1. rewrite <- env_replace; ms.
+    * apply p_contr; apply IHw; [simpl in *; lia|ms|rewrite union_difference_L; ms|].
+      apply (ImpLImp_prev _ φ1 φ2 φ3). exch 0.
+      peapply Hp2. rewrite <- env_replace; ms.
+  + rewrite union_difference_L in Hin' by ms.
+    forward. apply ImpLImp; backward.
+    * apply (IHh ψ Hle) with Hp1. lia. ms. ms.
+    * apply (IHh ψ Hle) with Hp2. lia. ms. ms.
+- case (decide (ψ = (□ φ1 → φ2))); intro Heq.
+  + subst. exhibit Hin' 0.
+    apply ImpBox.
+    * assert (Hr := open_boxes_remove _ _ Hin'). simpl in Hr. box_tac. symmetry in Hr. rw Hr 2.
+        clear Hr.
+        do 3 (exch 0; apply p_contr; apply IHw; [simpl in *; lia|ms|rewrite union_difference_L; ms|exch 1]).
+       exch 0.
+       assert(Heq : (⊗ (Γ • (□ φ1 → φ2)) ∖ {[□ φ1 → φ2]} ∖ {[□ φ1 → φ2]}) ≡ (⊗ (Γ∖ {[□ φ1 → φ2]})))
+       by (autorewrite with proof; simpl; ms).
+       rw Heq 5. clear Heq.
+       apply ImpBox_dup. exch 0; exch 1. peapply Hp1. rewrite open_boxes_remove; [|ms]. simpl.
+       rewrite <- difference_singleton. ms. apply open_boxes_spec'. left. simpl; split; trivial. ms.
+      * apply p_contr; apply IHw; [simpl in *; lia|ms|rewrite union_difference_L; ms|].
+         apply (ImpLBox_prev _ φ1 φ2). exch 0.
+         peapply Hp2. rewrite <- env_replace; ms.
+  + rewrite union_difference_L in Hin' by ms.
+      assert(Hinψ : ψ ∈ (Γ ∖ {[ψ]})) by ms. apply In_open_boxes in Hinψ.
+      forward. apply ImpBox. box_tac. exch 0; do 2 backward.
+      * rewrite open_boxes_remove in Hinψ by trivial.
+         case_eq (is_box ψ); intro Hψ.
+       -- apply is_box_weight_open_box in Hψ.
+          assert (Hle' : weight(⊙ψ) ≤ S w) by lia.
+          apply (IHh (⊙ ψ) Hle') with Hp1. lia. ms. ms.
+      -- apply is_not_box_open_box in Hψ. rewrite Hψ. apply IHh with Hp1.
+          trivial. lia. rewrite <- Hψ. ms. trivial. rewrite <- Hψ. ms.
+      * backward. apply (IHh ψ Hle) with Hp2. lia. ms. ms.
+- assert(Hinψ : ψ ∈ (Γ ∖ {[ψ]})) by ms. apply In_open_boxes in Hinψ.
+   rewrite open_boxes_remove in Hinψ by trivial.
+  apply BoxR. box_tac. backward. apply IHh with Hp.
+    etransitivity. apply weight_open_box. trivial.
+    lia.
+    ms.
+    ms.
+Qed.
+ +
+Global Hint Resolve contraction : proof.
+ +
+Theorem generalised_contraction (Γ Γ' : env) φ: Γ' ⊎ Γ' ⊎ Γ ⊢ φ -> Γ' ⊎ Γ ⊢ φ.
+Proof.
+revert Γ.
+induction Γ' as [| x Γ' IHΓ'] using gmultiset_rec; intros Γ Hp.
+- peapply Hp.
+- peapply (contraction (Γ' ⊎ Γ) x). peapply (IHΓ' (Γ•x•x)). peapply Hp.
+Qed.
+ +
+
+ +
+

Admissibility of LJ's implication left rule

+ +
+ + We show that the general implication left rule of LJ is admissible in G4ip. + This is Proposition 5.2 in (Dyckhoff Negri 2000). +
+
+ +
+Lemma ImpL Γ φ ψ θ: Γ•(φ → ψ) ⊢ φ -> Γ•ψ ⊢ θ -> Γ•(φ → ψ) ⊢ θ.
+Proof. intros H1 H2. apply contraction, weak_ImpL; auto with proof. Qed.
+ +
+(* Lemma 5.3 (Dyckhoff Negri 2000) shows that an implication on the left may be
+   weakened. *)
+ +
+Lemma imp_cut φ Γ ψ θ: Γ•(φ → ψ) ⊢ θ -> Γ•ψ ⊢ θ.
+Proof.
+intro Hp.
+remember (Γ•(φ → ψ)) as Γ0 eqn:HH.
+assert (Heq: Γ ≡ Γ0 ∖ {[(φ → ψ)]}) by ms.
+assert(Hin : (φ → ψ) ∈ Γ0) by ms. clear HH.
+rw Heq 1. clear Heq Γ.
+remember (weight φ) as w.
+assert(Hle : weight φ ≤ w) by lia.
+clear Heqw. revert Γ0 φ ψ θ Hle Hin Hp.
+induction w; intros Γ φ ψ θ Hle Hin Hp;
+ [destruct φ; simpl in Hle; lia|].
+induction Hp.
+- forward. auto with proof.
+- forward. auto with proof.
+-apply AndR; intuition.
+- forward; apply AndL. exch 0. do 2 backward. apply IHHp. ms.
+- apply OrR1; intuition.
+- apply OrR2; intuition.
+- forward. apply OrL; backward; [apply IHHp1 | apply IHHp2]; ms.
+- apply ImpR. backward. apply IHHp. ms.
+- case (decide ((p → φ0) = (φ → ψ))); intro Heq0.
+  + inversion Heq0; subst. peapply Hp.
+  + do 2 forward. exch 0. apply ImpLVar. exch 0. do 2 backward. apply IHHp; ms.
+- case (decide ((φ1 ∧ φ2 → φ3) = (φ → ψ))); intro Heq0.
+  + inversion Heq0; subst.
+    assert(Heq1 : ((Γ•(φ1 ∧ φ2 → ψ)) ∖ {[φ1 ∧ φ2 → ψ]}) ≡ Γ) by ms;
+    rw Heq1 1; clear Heq1. simpl in Hle.
+    peapply (IHw (Γ•(φ2 → ψ)) φ2 ψ ψ0); [lia|ms|].
+    peapply (IHw (Γ•(φ1 → φ2 → ψ)) φ1 (φ2 → ψ) ψ0); [lia|ms|trivial].
+  + forward. apply ImpLAnd. backward. apply IHHp. ms.
+- case (decide ((φ1 ∨ φ2 → φ3) = (φ → ψ))); intro Heq0.
+  + inversion Heq0. subst. clear Heq0.
+    apply contraction. simpl in Hle.
+    peapply (IHw (Γ•ψ•(φ1 → ψ)) φ1 ψ); [lia|ms|].
+    exch 0.
+    peapply (IHw (Γ•(φ1 → ψ)•(φ2 → ψ)) φ2 ψ); trivial; [lia|ms].
+  + forward. apply ImpLOr; exch 0; do 2 backward; apply IHHp; ms.
+- case (decide (((φ1 → φ2) → φ3) = (φ → ψ))); intro Heq0.
+  + inversion Heq0. subst. clear Heq0. peapply Hp2.
+  + forward. apply ImpLImp; backward; (apply IHHp1 || apply IHHp2); ms.
+- case (decide((□φ1 → φ2) = (φ → ψ))).
+  + intro Heq. inversion Heq. subst. clear Heq. peapply Hp2.
+  + intro Hneq. forward. apply ImpBox; repeat box_tac.
+      * exch 0. do 2 backward. apply open_box_L. apply IHHp1. ms.
+      * backward. apply IHHp2. ms.
+- apply BoxR. repeat box_tac. backward. apply open_box_L, IHHp.
+  apply env_in_add. right. auto with proof.
+Qed.
+ +
+Global Hint Resolve imp_cut : proof.
+ +
+
+ +
+

Correctness of optimizations

+ + +
+ +To make the definitions of the propositional quantifiers that we extract from the Coq definition more readable, we introduced functions "make_impl", "make_conj" and "make_disj" in Environments.v which perform obvious simplifications such as reducing φ ∧ ⊥ to ⊥ and φ ∨ ⊥ to φ. The following results show that the definitions of these functions are correct, in the sense that it does not make a difference for provability of a sequent whether one uses the literal conjunction, disjunction, and implication, or its optimized version. +
+
+ +
+Lemma make_impl_sound_L Γ φ ψ θ: Γ•(φ → ψ) ⊢ θ -> Γ•(φ ⇢ ψ) ⊢ θ.
+Proof.
+destruct (make_impl_spec φ ψ) as [[[Hm Heq]|[Hm Heq]]|Hm].
+- subst. rewrite Heq. intros Hp. apply TopL_rev in Hp. now apply weakening.
+- subst. rewrite Heq. intros Hp. now apply imp_cut in Hp.
+- now rewrite Hm.
+Qed.
+ +
+Global Hint Resolve make_impl_sound_L : proof.
+ +
+Lemma make_impl_sound_L2 Γ φ1 φ2 ψ θ: Γ•(φ1 → (φ2 → ψ)) ⊢ θ -> Γ•(φ1 ⇢ (φ2 ⇢ ψ)) ⊢ θ.
+Proof.
+destruct (make_impl_spec φ2 ψ) as [[[Hm Heq]|[Hm Heq]]|Hm].
+- subst. rewrite Heq. intro Hp. apply imp_cut, TopL_rev in Hp. auto with proof.
+- subst. rewrite Heq. intro Hp. apply imp_cut, imp_cut, TopL_rev in Hp. auto with proof.
+- rewrite Hm. apply make_impl_sound_L.
+Qed.
+ +
+Global Hint Resolve make_impl_sound_L2: proof.
+ +
+Lemma make_impl_sound_L2' Γ φ1 φ2 ψ θ: Γ•((φ1 → φ2) → ψ) ⊢ θ -> Γ•((φ1 ⇢ φ2) ⇢ ψ) ⊢ θ.
+Proof.
+destruct (make_impl_spec φ1 φ2) as [[[Hm Heq]|[Hm Heq]]|Hm].
+- subst. rewrite Heq.
+  destruct (make_impl_spec (¬ Bot) ψ) as [[[Hm Heq']|[Hm Heq']]|Hm].
+  + congruence.
+  + subst. intro Hp. apply imp_cut, TopL_rev in Hp. auto with proof.
+  + rewrite Hm. intro Hp. apply weak_ImpL.
+       * auto with proof.
+       * now apply imp_cut in Hp.
+- subst. rewrite Heq.
+  destruct (make_impl_spec (¬ Bot) ψ) as [[[Hm Heq']|[Hm Heq']]|Hm].
+  + congruence.
+  + subst. intro Hp. apply imp_cut, TopL_rev in Hp. auto with proof.
+  + rewrite Hm. intro Hp. apply weak_ImpL.
+       * auto with proof.
+       * now apply imp_cut in Hp.
+- rewrite Hm. clear Hm. destruct (make_impl_spec (φ1 → φ2) ψ) as [[[Hm Heq]|[Hm Heq]]|Hm].
+  + discriminate.
+  + subst. intro Hp. apply imp_cut, TopL_rev in Hp. auto with proof.
+  + now rewrite Hm.
+Qed.
+ +
+Lemma make_impl_complete_L Γ φ ψ θ: Γ•(φ ⇢ ψ) ⊢ θ -> Γ•(φ → ψ) ⊢ θ.
+Proof.
+destruct (make_impl_spec φ ψ) as [[[Hm Heq]|[Hm Heq]]|Hm].
+- subst. rewrite Heq. intros Hp. apply TopL_rev in Hp. now apply weakening.
+- subst. rewrite Heq. intros Hp. apply TopL_rev in Hp. now apply weakening.
+- now rewrite Hm.
+Qed.
+ +
+Lemma make_impl_complete_L2 Γ φ1 φ2 ψ θ: Γ•(φ1 ⇢ (φ2 ⇢ ψ)) ⊢ θ -> Γ•(φ1 → (φ2 → ψ)) ⊢ θ.
+Proof.
+destruct (make_impl_spec φ2 ψ) as [[[Hm Heq]|[Hm Heq]]|Hm].
+- subst. rewrite Heq. intro Hp. apply make_impl_complete_L in Hp.
+  apply imp_cut, TopL_rev in Hp. now apply weakening.
+- subst. rewrite Heq. intro Hp. apply make_impl_complete_L in Hp.
+  apply imp_cut, TopL_rev in Hp. now apply weakening.
+- rewrite Hm. apply make_impl_complete_L.
+Qed.
+ +
+Lemma make_impl_complete_R Γ φ ψ: Γ ⊢ φ ⇢ ψ -> Γ ⊢ (φ → ψ).
+Proof.
+destruct (make_impl_spec φ ψ) as [[[Hm Heq]|[Hm Heq]]|Hm]; subst; auto with proof.
+now rewrite Hm.
+Qed.
+ +
+Lemma make_impl_sound_R Γ φ ψ: Γ ⊢ (φ → ψ) -> Γ ⊢ φ ⇢ ψ.
+Proof.
+destruct (make_impl_spec φ ψ) as [[[Hm Heq]|[Hm Heq]]|Heq]; subst; rewrite Heq; auto with proof.
+Qed.
+ +
+Global Hint Resolve make_impl_sound_R : proof.
+ +
+Lemma make_disj_sound_L Γ φ ψ θ : Γ•φ ∨ψ ⊢ θ -> Γ•make_disj φ ψ ⊢ θ.
+Proof.
+intro Hd. apply OrL_rev in Hd as (Hφ&Hψ). unfold make_disj.
+destruct φ; trivial;
+try (destruct ψ; try case decide; trivial; auto 2 with proof; destruct ψ1; auto 2 with proof; destruct ψ2; auto 2 with proof).
+destruct φ1; destruct φ2; destruct ψ; trivial; case decide; intro Heq; try inversion Heq; auto 2 with proof ; destruct ψ1; auto 2 with proof;
+destruct ψ2; auto 2 with proof.
+Qed.
+ +
+Global Hint Resolve make_disj_sound_L : proof.
+ +
+Lemma make_disj_complete Γ φ ψ θ : Γ•make_disj φ ψ ⊢ θ -> Γ•φ ∨ψ ⊢ θ.
+Proof.
+destruct (make_disj_spec φ ψ) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm].
+6: { now rewrite Hm. }
+all : destruct Hm as (Heq&Hm); rewrite Hm; subst; eauto 2 with proof.
+Qed.
+ +
+Lemma make_conj_sound_L Γ φ ψ θ : Γ•φ ∧ψ ⊢ θ -> Γ•make_conj φ ψ ⊢ θ.
+Proof.
+intro Hd. apply AndL_rev in Hd.
+destruct (make_conj_spec φ ψ) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm].
+6:{ rewrite Hm. now apply AndL. }
+all:(destruct Hm as [Heq Hm]; rewrite Hm; subst; auto with proof).
+- eapply TopL_rev. exch 0. exact Hd.
+- eapply TopL_rev. exact Hd.
+Qed.
+ +
+Global Hint Resolve make_conj_sound_L : proof.
+ +
+Lemma make_conj_complete_L Γ φ ψ θ : Γ•make_conj φ ψ ⊢ θ -> Γ•φ ∧ψ ⊢ θ.
+Proof.
+destruct (make_conj_spec φ ψ) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm].
+6:{ now rewrite Hm. }
+all:(destruct Hm as [Heq Hm]; rewrite Hm; subst; auto with proof).
+Qed.
+ +
+Lemma make_conj_sound_R Γ φ ψ : Γ ⊢ φ ∧ψ -> Γ ⊢ make_conj φ ψ.
+Proof.
+intro Hd. apply AndR_rev in Hd.
+destruct (make_conj_spec φ ψ) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm].
+6:{ rewrite Hm. apply AndR; tauto. }
+all:(destruct Hm as [Heq Hm]; rewrite Hm; subst; tauto).
+Qed.
+ +
+Global Hint Resolve make_conj_sound_R : proof.
+ +
+Lemma make_conj_complete_R Γ φ ψ : Γ ⊢ make_conj φ ψ -> Γ ⊢ φ ∧ψ.
+Proof.
+destruct (make_conj_spec φ ψ) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm].
+6:{ now rewrite Hm. }
+all:(destruct Hm as [Heq Hm]; rewrite Hm; subst; auto with proof).
+Qed.
+ +
+Lemma OrR_idemp Γ ψ : Γ ⊢ ψ ∨ ψ -> Γ ⊢ ψ.
+Proof. intro Hp. dependent induction Hp; auto with proof. Qed.
+ +
+Lemma make_disj_sound_R Γ φ ψ : Γ ⊢ φ ∨ψ -> Γ ⊢ make_disj φ ψ.
+Proof.
+intro Hd.
+destruct (make_disj_spec φ ψ) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm].
+6:{ now rewrite Hm. }
+all:(destruct Hm as [Heq Hm]; rewrite Hm; subst; auto using OrR2Bot_rev, OrR1Bot_rev with proof).
+now apply OrR_idemp.
+Qed.
+ +
+Global Hint Resolve make_disj_sound_R : proof.
+ +
+Lemma make_disj_complete_R Γ φ ψ : Γ ⊢ make_disj φ ψ -> Γ ⊢ φ ∨ψ.
+Proof.
+destruct (make_disj_spec φ ψ) as [[[[[Hm|Hm]|Hm]|Hm]|Hm]|Hm].
+6:{ now rewrite Hm. }
+all:(destruct Hm as [Heq Hm]; rewrite Hm; subst; auto using exfalso with proof).
+Qed.
+ +
+
+ +
+

Generalized rules

+ + +
+ +In this section we prove that generalizations of or-left and and-right rules +that take more than two formulas are admissible and invertible in the calculus +G4ip. This is important in the correctness proof of propositional quantifiers +because the propositional quantifiers are defined as large disjunctions / +conjunctions of various individual formulas. + +
+ +

Generalized OrL and its invertibility

+ +
+
+ +
+Lemma disjunction_L Γ Δ θ :
+  ((forall φ, φ ∈ Δ -> (Γ•φ ⊢ θ)) -> (Γ•⋁ Δ ⊢ θ)) *
+  ((Γ•⋁ Δ ⊢ θ) -> (forall φ, φ ∈ Δ -> (Γ•φ ⊢ θ))).
+Proof.
+unfold disjunction.
+assert(Hcut :
+  (forall ψ, (Γ•ψ ⊢ θ) -> (forall φ, φ ∈ Δ -> (Γ•φ ⊢ θ)) ->
+    (Γ•foldl make_disj ψ (nodup form_eq_dec Δ) ⊢ θ)) *
+  (forall ψ,((Γ•foldl make_disj ψ (nodup form_eq_dec Δ)) ⊢ θ ->
+    (Γ•ψ ⊢ θ) * (∀ φ : form, φ ∈ Δ → (Γ•φ) ⊢ θ)))).
+{
+  induction Δ; simpl; split; intros ψ Hψ.
+  - intro. apply Hψ.
+  - split; trivial. intros φ Hin. contradict Hin. auto with *.
+  - intro Hall. case in_dec; intro; apply (fst IHΔ); auto with *.
+  - case in_dec in Hψ; apply IHΔ in Hψ;
+    destruct Hψ as [Hψ Hind].
+    + split; trivial; intros φ Hin; destruct (decide (φ = a)); auto with *.
+        subst. apply Hind. now apply elem_of_list_In.
+    + apply make_disj_complete in Hψ.
+        apply OrL_rev in Hψ as [Hψ Ha].
+        split; trivial; intros φ Hin; destruct (decide (φ = a)); auto with *.
+}
+split; apply Hcut. constructor 2.
+Qed.
+ +
+
+ +
+

Generalized AndR

+ +
+
+ +
+Lemma conjunction_R1 Γ Δ : (forall φ, φ ∈ Δ -> Γ ⊢ φ) -> (Γ ⊢ ⋀ Δ).
+Proof.
+intro Hprov. unfold conjunction.
+assert(Hcut : forall θ, Γ ⊢ θ -> Γ ⊢ foldl make_conj θ (nodup form_eq_dec Δ)).
+{
+  induction Δ; intros θ Hθ; simpl; trivial.
+  case in_dec; intro; auto with *.
+  apply IHΔ.
+  - intros; apply Hprov. now right.
+  - apply make_conj_sound_R, AndR; trivial. apply Hprov. now left.
+}
+apply Hcut. apply ImpR, ExFalso.
+Qed.
+ +
+
+ +
+

Generalized invertibility of AndR

+ +
+
+ +
+Lemma conjunction_R2 Γ Δ : (Γ ⊢ ⋀ Δ) -> (forall φ, φ ∈ Δ -> Γ ⊢ φ).
+Proof.
+ unfold conjunction.
+assert(Hcut : forall θ, Γ ⊢ foldl make_conj θ (nodup form_eq_dec Δ) -> (Γ ⊢ θ) * (forall φ, φ ∈ Δ -> Γ ⊢ φ)).
+{
+  induction Δ; simpl; intros θ Hθ.
+  - split; trivial. intros φ Hin; contradict Hin. auto with *.
+  - case in_dec in Hθ; destruct (IHΔ _ Hθ) as (Hθ' & Hi);
+     try (apply make_conj_complete_R in Hθ'; destruct (AndR_rev Hθ')); split; trivial;
+     intros φ Hin; apply elem_of_cons in Hin;
+     destruct (decide (φ = a)); subst; trivial.
+     + apply Hi. rewrite elem_of_list_In; tauto.
+     + apply (IHΔ _ Hθ). tauto.
+     + apply (IHΔ _ Hθ). tauto.
+}
+apply Hcut.
+Qed.
+ +
+
+ +
+

Generalized AndL

+ +
+
+ +
+Lemma conjunction_L Γ Δ φ θ: (φ ∈ Δ) -> (Γ•φ ⊢ θ) -> (Γ•⋀ Δ ⊢ θ).
+Proof.
+intros Hin Hprov. unfold conjunction. revert Hin.
+assert(Hcut : forall ψ, ((φ ∈ Δ) + (Γ•ψ ⊢ θ)) -> (Γ•foldl make_conj ψ (nodup form_eq_dec Δ) ⊢ θ)).
+{
+  induction Δ; simpl; intros ψ [Hin | Hψ].
+  - contradict Hin; auto with *.
+  - trivial.
+  - case in_dec; intro; apply IHΔ; destruct (decide (φ = a)).
+    + subst. left. now apply elem_of_list_In.
+    + left. auto with *.
+    + subst. right. apply make_conj_sound_L. auto with proof.
+    + left. auto with *.
+  - case in_dec; intro; apply IHΔ; right; trivial.
+     apply make_conj_sound_L. auto with proof.
+}
+intro Hin. apply Hcut. now left.
+Qed.
+ +
+
+ +
+

Generalized OrR

+ +
+
+ +
+Lemma disjunction_R Γ Δ φ : (φ ∈ Δ) -> (Γ ⊢ φ) -> (Γ ⊢ ⋁ Δ).
+Proof.
+intros Hin Hprov. unfold disjunction. revert Hin.
+assert(Hcut : forall θ, ((Γ ⊢ θ) + (φ ∈ Δ)) -> Γ ⊢ foldl make_disj θ (nodup form_eq_dec Δ)).
+{
+  induction Δ; simpl; intros θ [Hθ | Hin].
+  - assumption.
+  - contradict Hin; auto with *.
+  - case in_dec; intro; apply IHΔ; left; trivial. apply make_disj_sound_R. now apply OrR1.
+  - apply elem_of_cons in Hin.
+    destruct (decide (φ = a)).
+    + subst. case in_dec; intro; apply IHΔ.
+        * right. now apply elem_of_list_In.
+        * left. apply make_disj_sound_R. now apply OrR2.
+    + case in_dec; intro; apply IHΔ; right; tauto.
+}
+intro Hin. apply Hcut; now right.
+Qed.
+ +
+Lemma strongness φ : ∅ • φ ⊢ □ φ.
+Proof.
+apply BoxR. box_tac. apply weakening, open_box_L, generalised_axiom.
+Qed.
+
+
+ +
+ + + diff --git a/html/ISL.Sequents.html b/html/ISL.Sequents.html new file mode 100644 index 0000000..dab3149 --- /dev/null +++ b/html/ISL.Sequents.html @@ -0,0 +1,305 @@ + + + + + + + + + + + + + +
+
+

ISL.Sequents

+ +
+Require Export ISL.Environments.
+ +
+Import EnvMS.
+ +
+Open Scope stdpp_scope.
+ +
+
+ +
+

Overview: Sequent calculus G4ip

+ +
+ + We implement the sequent calculus G4ip, a contraction-free + refinement of the usual Gentzen sequent calculus LJ for intuitionistic + propositional logic, which was developed by the Soviet school of proof theory + (Vorob'ev 1970) and introduced in the West by (Hudelmaier 1989) and (Dyckhoff + 1990). This calculus is also referred to as "LJT" in the literature, but we this name has also been used in the literature for other, unrelated calculi, so we prefer to use "G4ip" to avoid ambiguity. + +
+ + The calculus G4ip is important because it allows for a terminating proof + search, and in our proof of Pitts' theorem, it therefore lets us perform + well-founded induction on proofs. Technically, this is thanks to the absence of + a contraction rule. The left implication rule is refined into four separate + proof rules. +
+ +

Definition of provability in G4iSL

+ +
+
+Reserved Notation "Γ ⊢ φ" (at level 90).
+Inductive Provable : env -> form -> Type :=
+| Atom : ∀ Γ p, Γ • (Var p) ⊢ (Var p)
+| ExFalso : ∀ Γ φ, Γ • ⊥ ⊢ φ
+| AndR : ∀ Γ φ ψ,
+    Γ ⊢ φ -> Γ ⊢ ψ ->
+      Γ ⊢ (φ ∧ ψ)
+| AndL : ∀ Γ φ ψ θ,
+    Γ • φ • ψ ⊢ θ ->
+      Γ • (φ ∧ ψ) ⊢ θ
+| OrR1 : ∀ Γ φ ψ,
+    Γ ⊢ φ ->
+      Γ ⊢ (φ ∨ ψ)
+| OrR2 : ∀ Γ φ ψ,
+    Γ ⊢ ψ ->
+      Γ ⊢ (φ ∨ ψ)
+| OrL : ∀ Γ φ ψ θ,
+    Γ • φ ⊢ θ -> Γ • ψ ⊢ θ ->
+      Γ • (φ ∨ ψ) ⊢ θ
+| ImpR : ∀ Γ φ ψ,
+    Γ • φ ⊢ ψ ->
+      Γ ⊢ (φ → ψ)
+| ImpLVar : ∀ Γ p φ ψ,
+    Γ • Var p • φ ⊢ ψ ->
+      Γ • Var p • (Var p → φ) ⊢ ψ
+| ImpLAnd : ∀ Γ φ1 φ2 φ3 ψ,
+    Γ • (φ1 → (φ2 → φ3)) ⊢ ψ ->
+      Γ • ((φ1 ∧ φ2) → φ3) ⊢ ψ
+| ImpLOr : ∀ Γ φ1 φ2 φ3 ψ,
+    Γ • (φ1 → φ3) • (φ2 → φ3) ⊢ ψ ->
+      Γ • ((φ1 ∨ φ2) → φ3) ⊢ ψ
+| ImpLImp : ∀ Γ φ1 φ2 φ3 ψ,
+    Γ • (φ2 → φ3) ⊢ (φ1 → φ2) ->Γ • φ3 ⊢ ψ ->
+      Γ • ((φ1 → φ2) → φ3) ⊢ ψ
+| ImpBox : ∀ Γ φ1 φ2 ψ,
+    (⊗ Γ) • □ φ1 • φ2 ⊢ φ1 ->
+    Γ • φ2 ⊢ ψ ->
+      Γ • ((□ φ1) → φ2) ⊢ ψ
+| BoxR : ∀ Γ φ, open_boxes Γ • □ φ ⊢ φ -> Γ ⊢ □ φ
+where "Γ ⊢ φ" := (Provable Γ φ).
+ +
+Global Hint Constructors Provable : proof.
+ +
+
+ +
+We show that equivalent multisets prove the same things. +
+
+Global Instance proper_Provable : Proper ((≡@{env}) ==> (=) ==> (=)) Provable.
+Proof. intros Γ Γ' Heq φ φ' Heq'. ms. Qed.
+ +
+
+ +
+We introduce a tactic "peapply" which allows for application of a G4ip rule + even in case the environment needs to be reordered +
+
+Ltac peapply th :=
+  (erewrite proper_Provable; [| |reflexivity]); [eapply th|try ms].
+ +
+
+ +
+

Tactics

+ +
+ + We introduce a few tactics that we will need to prove the admissibility of + the weakening and exchange rules in the proof calculus. +
+ + The tactic "exch" swaps the nth pair of formulas of a sequent, counting from the right. +
+
+ +
+Ltac exch n := match n with
+| O => rewrite (proper_Provable _ _ (env_add_comm _ _ _) _ _ eq_refl)
+| S O => rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (env_add_comm _ _ _)) _ _ eq_refl)
+| S (S O) => rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_add_comm _ _ _))) _ _ eq_refl)
+| S (S (S O)) => rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_add_comm _ _ _)))) _ _ eq_refl)
+end.
+ +
+
+ +
+The tactic "exhibit" exhibits an element that is in the environment. +
+
+Ltac exhibit Hin n := match n with
+| 0 => rewrite (proper_Provable _ _ (difference_singleton _ _ Hin) _ _ eq_refl)
+| 1 => rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (difference_singleton _ _ Hin)) _ _ eq_refl)
+| 2 => rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat_r (difference_singleton _ _ Hin))) _ _ eq_refl)
+| 3 => rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (difference_singleton _ _ Hin)))) _ _ eq_refl)
+end.
+ +
+
+ +
+The tactic "forward" tries to change a goal of the form : + +
+ +((Γ•φ ∖ {ψ}•…) ⊢ … + +
+ +into + +
+ +((Γ ∖ {ψ}•…•φ) ⊢ … , + +
+ +by first proving that ψ ∈ Γ. +
+
+ +
+Ltac forward := match goal with
+| |- (?Γ•?φ) ∖ {[?ψ]} ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by ms;
+  rewrite (proper_Provable _ _ (env_replace φ Hin) _ _ eq_refl)
+| |- (?Γ•?φ) ∖ {[?ψ]}•_ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by ms;
+  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (env_replace φ Hin)) _ _ eq_refl);
+  exch 0
+| |- (?Γ•?φ) ∖ {[?ψ]}•_•_ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by ms;
+  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin))) _ _ eq_refl);
+  exch 1; exch 0
+| |- (?Γ•?φ) ∖ {[?ψ]}•_•_•_ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by ms;
+  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin)))) _ _ eq_refl);
+  exch 2; exch 1; exch 0
+| |- (?Γ•?φ) ∖ {[?ψ]}•_•_•_•_ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by ms;
+  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin))))) _ _ eq_refl);
+  exch 3; exch 2; exch 1; exch 0
+end.
+ +
+
+ +
+The tactic "backward" changes a goal of the form : + +
+ +((Γ ∖ {ψ}•…•φ) ⊢ … + +
+ +into + +
+ +((Γ•φ ∖ {ψ}•…) ⊢ …, + +
+ +by first proving that ψ ∈ Γ. + +
+ + +
+
+ +
+Ltac backward := match goal with
+| |- ?Γ ∖ {[?ψ]}•?φ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by (ms || auto with proof);
+  rewrite (proper_Provable _ _ (symmetry(env_replace _ Hin)) _ _ eq_refl)
+| |- ?Γ ∖ {[?ψ]}•_•?φ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by (ms || auto with proof); try exch 0;
+  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r (env_replace _ Hin))) _ _ eq_refl)
+| |- ?Γ ∖ {[?ψ]}•_•_•?φ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by (ms || auto with proof); exch 0; exch 1;
+  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin)))) _ _ eq_refl)
+| |- ?Γ ∖ {[?ψ]}•_•_•_•?φ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by (ms || auto with proof); exch 0; exch 1; exch 2;
+  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin))))) _ _ eq_refl)
+| |- ?Γ ∖ {[?ψ]}•_•_•_•_•?φ ⊢ _ =>
+  let Hin := fresh "Hin" in
+  assert(Hin : ψ ∈ Γ) by (ms || auto with proof); exch 0; exch 1; exch 2; exch 3;
+  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin)))))) _ _ eq_refl)
+end.
+ +
+
+ +
+The tactic "rw" rewrites the environment equivalence Heq under the nth formula in the premise. +
+
+Ltac rw Heq n := match n with
+| 0 => erewrite (proper_Provable _ _ Heq _ _ eq_refl)
+| 1 => erewrite (proper_Provable _ _ (equiv_disj_union_compat_r Heq) _ _ eq_refl)
+| 2 => erewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r Heq)) _ _ eq_refl)
+| 3 => erewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r Heq))) _ _ eq_refl)
+| 4 => erewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r Heq)))) _ _ eq_refl)
+| 5 => erewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r Heq))))) _ _ eq_refl)
+end.
+ +
+Ltac box_tac :=
+       let rec box_tac_aux Δ n := lazymatch Δ with
+  |⊗(?Δ' • ?φ) => rewrite (open_boxes_add Δ' φ)
+  |⊗(?Γ ∖ {[?ψ]}) => match goal with |H: ψ ∈ Γ |- _ => rw (open_boxes_remove Γ ψ H) n end
+  | ?Δ' • ?φ => box_tac_aux Δ' (S n) end
+  in
+    try match goal with | |- ?Δ ⊢ _ => box_tac_aux Δ 0 end; simpl.
+
+
+ +
+ + + diff --git a/html/config.js b/html/config.js new file mode 100644 index 0000000..72be613 --- /dev/null +++ b/html/config.js @@ -0,0 +1,72 @@ +var coqdocjs = coqdocjs || {}; + +coqdocjs.repl = { + "forall": "∀", + "exists": "∃", + "~": "¬", + "/\\": "∧", + "\\/": "∨", + "->": "→", + "<-": "←", + "<->": "↔", + "=>": "⇒", + "<>": "≠", + "<=": "≤", + ">=": "≥", + "el": "∈", + "nel": "∉", + "<<=": "⊆", + "|-": "⊢", + ">>": "»", + "<<": "⊆", + "++": "⧺", + "===": "≡", + "=/=": "≢", + "=~=": "≅", + "==>": "⟹", + "lhd": "⊲", + "rhd": "⊳", + "nat": "ℕ", + "alpha": "α", + "beta": "β", + "gamma": "γ", + "delta": "δ", + "epsilon": "ε", + "eta": "η", + "iota": "ι", + "kappa": "κ", + "lambda": "λ", + "mu": "μ", + "nu": "ν", + "omega": "ω", + "phi": "ϕ", + "pi": "π", + "psi": "ψ", + "rho": "ρ", + "sigma": "σ", + "tau": "τ", + "theta": "θ", + "xi": "ξ", + "zeta": "ζ", + "Delta": "Δ", + "Gamma": "Γ", + "Pi": "Π", + "Sigma": "Σ", + "Omega": "Ω", + "Xi": "Ξ" +}; + +coqdocjs.subscr = { + "0" : "₀", + "1" : "₁", + "2" : "₂", + "3" : "₃", + "4" : "₄", + "5" : "₅", + "6" : "₆", + "7" : "₇", + "8" : "₈", + "9" : "₉", +}; + +coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="]; diff --git a/html/coqdoc.css b/html/coqdoc.css new file mode 100644 index 0000000..18dad89 --- /dev/null +++ b/html/coqdoc.css @@ -0,0 +1,197 @@ +@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700); + +body{ + font-family: 'Open Sans', sans-serif; + font-size: 14px; + color: #2D2D2D +} + +a { + text-decoration: none; + border-radius: 3px; + padding-left: 3px; + padding-right: 3px; + margin-left: -3px; + margin-right: -3px; + color: inherit; + font-weight: bold; +} + +#main .code a, #main .inlinecode a, #toc a { + font-weight: inherit; +} + +a[href]:hover, [clickable]:hover{ + background-color: rgba(0,0,0,0.1); + cursor: pointer; +} + +h, h1, h2, h3, h4, h5 { + line-height: 1; + color: black; + text-rendering: optimizeLegibility; + font-weight: normal; + letter-spacing: 0.1em; + text-align: left; +} + +div + br { + display: none; +} + +div:empty{ display: none;} + +#main h1 { + font-size: 2em; +} + +#main h2 { + font-size: 1.667rem; +} + +#main h3 { + font-size: 1.333em; +} + +#main h4, #main h5, #main h6 { + font-size: 1em; +} + +#toc h2 { + padding-bottom: 0; +} + +#main .doc { + margin: 0; + text-align: justify; +} + +.inlinecode, .code, #main pre { + font-family: monospace; +} + +.code > br:first-child { + display: none; +} + +.doc + .code{ + margin-top:0.5em; +} + +.block{ + display: block; + margin-top: 5px; + margin-bottom: 5px; + padding: 10px; + text-align: center; +} + +.block img{ + margin: 15px; +} + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; + text-align: center; + padding: 0; + line-height: 1; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + padding-left: 1em; + padding-bottom: 0.1em +} + +.id[type="constructor"], .id[type="projection"], .id[type="method"], +.id[title="constructor"], .id[title="projection"], .id[title="method"] { + color: #A30E16; +} + +.id[type="var"], .id[type="variable"], +.id[title="var"], .id[title="variable"] { + color: inherit; +} + +.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"], +.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] { + color: #A6650F; +} + +.id[type="lemma"], +.id[title="lemma"]{ + color: #188B0C; +} + +.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"], +.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{ + color : #2874AE; +} + +.comment { + color: #808080; +} + +/* TOC */ + +#toc h2{ + letter-spacing: 0; + font-size: 1.333em; +} + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; +} + +#index #frontispiece { + margin: 1em auto; + padding: 1em; + width: 60%; +} + +.booktitle { font-size : 140% } +.authors { font-size : 90%; + line-height: 115%; } +.moreauthors { font-size : 60% } + +#index #entrance { + text-align: center; +} + +#index #entrance .spacer { + margin: 0 30px 0 30px; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} + +#toc > * { + clear: both; +} + +#toc > a { + display: block; + float: left; + margin-top: 1em; +} + +#toc a h2{ + display: inline; +} diff --git a/html/coqdocjs.css b/html/coqdocjs.css new file mode 100644 index 0000000..d94bb58 --- /dev/null +++ b/html/coqdocjs.css @@ -0,0 +1,249 @@ +/* replace unicode */ + +.id[repl] .hidden { + font-size: 0; +} + +.id[repl]:before{ + content: attr(repl); +} + +/* folding proofs */ + +@keyframes show-proof { + 0% { + max-height: 1.2em; + opacity: 1; + } + 99% { + max-height: 1000em; + } + 100%{ + } +} + +@keyframes hide-proof { + from { + visibility: visible; + max-height: 10em; + opacity: 1; + } + to { + max-height: 1.2em; + } +} + +.proof { + cursor: pointer; +} +.proof * { + cursor: pointer; +} + +.proof { + overflow: hidden; + position: relative; + transition: opacity 1s; + display: inline-block; +} + +.proof[show="false"] { + max-height: 1.2em; + visibility: visible; + opacity: 0.3; +} + +.proof[show="false"][animate] { + animation-name: hide-proof; + animation-duration: 0.25s; +} + +.proof[show=true] { + animation-name: show-proof; + animation-duration: 10s; +} + +.proof[show="false"]:before { + position: absolute; + visibility: visible; + width: 100%; + height: 100%; + display: block; + opacity: 0; + content: "M"; +} +.proof[show="false"]:hover:before { + content: ""; +} + +.proof[show="false"] + br + br { + display: none; +} + +.proof[show="false"]:hover { + visibility: visible; + opacity: 0.5; +} + +#toggle-proofs[proof-status="no-proofs"] { + display: none; +} + +#toggle-proofs[proof-status="some-hidden"]:before { + content: "Show Proofs"; +} + +#toggle-proofs[proof-status="all-shown"]:before { + content: "Hide Proofs"; +} + + +/* page layout */ + +html, body { + height: 100%; + margin:0; + padding:0; +} + +@media only screen { /* no div with internal scrolling to allow printing of whole content */ + body { + display: flex; + flex-direction: column + } + + #content { + flex: 1; + overflow: auto; + display: flex; + flex-direction: column; + } +} + +#content:focus { + outline: none; /* prevent glow in OS X */ +} + +#main { + display: block; + padding: 16px; + padding-top: 1em; + padding-bottom: 2em; + margin-left: auto; + margin-right: auto; + max-width: 60em; + flex: 1 0 auto; +} + +.libtitle { + display: none; +} + +/* header */ +#header { + width:100%; + padding: 0; + margin: 0; + display: flex; + align-items: center; + background-color: rgb(21,57,105); + color: white; + font-weight: bold; + overflow: hidden; +} + + +.button { + cursor: pointer; +} + +#header * { + text-decoration: none; + vertical-align: middle; + margin-left: 15px; + margin-right: 15px; +} + +#header > .right, #header > .left { + display: flex; + flex: 1; + align-items: center; +} +#header > .left { + text-align: left; +} +#header > .right { + flex-direction: row-reverse; +} + +#header a, #header .button { + color: white; + box-sizing: border-box; +} + +#header a { + border-radius: 0; + padding: 0.2em; +} + +#header .button { + background-color: rgb(63, 103, 156); + border-radius: 1em; + padding-left: 0.5em; + padding-right: 0.5em; + margin: 0.2em; +} + +#header a:hover, #header .button:hover { + background-color: rgb(181, 213, 255); + color: black; +} + +#header h1 { padding: 0; + margin: 0;} + +/* footer */ +#footer { + text-align: center; + opacity: 0.5; + font-size: 75%; +} + +/* hyperlinks */ + +@keyframes highlight { + 50%{ + background-color: black; + } +} + +:target * { + animation-name: highlight; + animation-duration: 1s; +} + +a[name]:empty { + float: right; +} + +/* Proviola */ + +div.code { + width: auto; + float: none; +} + +div.goal { + position: fixed; + left: 75%; + width: 25%; + top: 3em; +} + +div.doc { + clear: both; +} + +span.command:hover { + background-color: inherit; +} diff --git a/html/coqdocjs.js b/html/coqdocjs.js new file mode 100644 index 0000000..10dc0bb --- /dev/null +++ b/html/coqdocjs.js @@ -0,0 +1,189 @@ +var coqdocjs = coqdocjs || {}; +(function(){ + +function replace(s){ + var m; + if (m = s.match(/^(.+)'/)) { + return replace(m[1])+"'"; + } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) { + return replace(m[1])+m[2].replace(/\d/g, function(d){ + if (coqdocjs.subscr.hasOwnProperty(d)) { + return coqdocjs.subscr[d]; + } else { + return d; + } + }); + } else if (coqdocjs.repl.hasOwnProperty(s)){ + return coqdocjs.repl[s] + } else { + return s; + } +} + +function toArray(nl){ + return Array.prototype.slice.call(nl); +} + +function replInTextNodes() { + coqdocjs.replInText.forEach(function(toReplace){ + toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){ + toArray(elem.childNodes).forEach(function(node){ + if (node.nodeType != Node.TEXT_NODE) return; + var fragments = node.textContent.split(toReplace); + node.textContent = fragments[fragments.length-1]; + for (var k = 0; k < fragments.length - 1; ++k) { + node.parentNode.insertBefore(document.createTextNode(fragments[k]),node); + var replacement = document.createElement("span"); + replacement.appendChild(document.createTextNode(toReplace)); + replacement.setAttribute("class", "id"); + replacement.setAttribute("type", "keyword"); + node.parentNode.insertBefore(replacement, node); + } + }); + }); + }); +} + +function replNodes() { + toArray(document.getElementsByClassName("id")).forEach(function(node){ + if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){ + var text = node.textContent; + var replText = replace(text); + if(text != replText) { + node.setAttribute("repl", replText); + node.setAttribute("title", text); + var hidden = document.createElement("span"); + hidden.setAttribute("class", "hidden"); + while (node.firstChild) { + hidden.appendChild(node.firstChild); + } + node.appendChild(hidden); + } + } + }); +} + +function isVernacStart(l, t){ + t = t.trim(); + for(var s of l){ + if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){ + return true; + } + } + return false; +} + +function isProofStart(n){ + return isVernacStart(["Proof"], n.textContent) || + (isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent)); +} + +function isProofEnd(s){ + return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s); +} + +function proofStatus(){ + var proofs = toArray(document.getElementsByClassName("proof")); + if(proofs.length) { + for(var proof of proofs) { + if (proof.getAttribute("show") === "false") { + return "some-hidden"; + } + } + return "all-shown"; + } + else { + return "no-proofs"; + } +} + +function updateView(){ + document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus()); +} + +function foldProofs() { + var hasCommands = true; + var nodes = document.getElementsByClassName("command"); + if(nodes.length == 0) { + hasCommands = false; + console.log("no command tags found") + nodes = document.getElementsByClassName("id"); + } + toArray(nodes).forEach(function(node){ + if(isProofStart(node)) { + var proof = document.createElement("span"); + proof.setAttribute("class", "proof"); + + node.parentNode.insertBefore(proof, node); + if(proof.previousSibling.nodeType === Node.TEXT_NODE) + proof.appendChild(proof.previousSibling); + while(node && !isProofEnd(node.textContent)) { + proof.appendChild(node); + node = proof.nextSibling; + } + if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed + if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed + + proof.addEventListener("click", function(proof){return function(e){ + if (e.target.parentNode.tagName.toLowerCase() === "a") + return; + proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true"); + proof.setAttribute("animate", ""); + updateView(); + };}(proof)); + proof.setAttribute("show", "false"); + } + }); +} + +function toggleProofs(){ + var someProofsHidden = proofStatus() === "some-hidden"; + toArray(document.getElementsByClassName("proof")).forEach(function(proof){ + proof.setAttribute("show", someProofsHidden); + proof.setAttribute("animate", ""); + }); + updateView(); +} + +function repairDom(){ + // pull whitespace out of command + toArray(document.getElementsByClassName("command")).forEach(function(node){ + while(node.firstChild && node.firstChild.textContent.trim() == ""){ + console.log("try move"); + node.parentNode.insertBefore(node.firstChild, node); + } + }); + toArray(document.getElementsByClassName("id")).forEach(function(node){ + node.setAttribute("type", node.getAttribute("title")); + }); + toArray(document.getElementsByClassName("idref")).forEach(function(ref){ + toArray(ref.childNodes).forEach(function(child){ + if (["var", "variable"].indexOf(child.getAttribute("type")) > -1) + ref.removeAttribute("href"); + }); + }); + +} + +function fixTitle(){ + var url = "/" + window.location.pathname; + var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.')); + if (basename === "toc") {document.title = "Table of Contents";} + else if (basename === "indexpage") {document.title = "Index";} + else {document.title = basename;} +} + +function postprocess(){ + repairDom(); + replInTextNodes() + replNodes(); + foldProofs(); + document.getElementById("toggle-proofs").addEventListener("click", toggleProofs); + updateView(); +} + +fixTitle(); +document.addEventListener('DOMContentLoaded', postprocess); + +coqdocjs.toggleProofs = toggleProofs; +})(); diff --git a/html/indexpage.html b/html/indexpage.html new file mode 100644 index 0000000..ef5d2be --- /dev/null +++ b/html/indexpage.html @@ -0,0 +1,1382 @@ + + + + + + + + + + + + + +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(271 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(21 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(5 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(138 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(25 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(7 entries)
Instance IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(17 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(48 entries)
+
+

Global Index

+

A

+A [definition, in ISL.PropQuantifiers]
+Af [definition, in ISL.PropQuantifiers]
+And [constructor, in ISL.Formulas]
+AndL [constructor, in ISL.Sequents]
+AndL_rev [lemma, in ISL.SequentProps]
+AndR [constructor, in ISL.Sequents]
+AndR_rev [lemma, in ISL.SequentProps]
+assoc_meq_union [instance, in ISL.Order]
+Atom [constructor, in ISL.Sequents]
+A_right [lemma, in ISL.PropQuantifiers]
+a_rule_env_spec [lemma, in ISL.PropQuantifiers]
+a_rule_form_vars [lemma, in ISL.PropQuantifiers]
+a_rule_env_vars [lemma, in ISL.PropQuantifiers]
+A_eq [definition, in ISL.PropQuantifiers]
+a_rule_form_cong [lemma, in ISL.PropQuantifiers]
+a_rule_env_cong [lemma, in ISL.PropQuantifiers]
+a_rule_form [definition, in ISL.PropQuantifiers]
+a_rule_env [definition, in ISL.PropQuantifiers]
+

B

+Bot [constructor, in ISL.Formulas]
+Box [constructor, in ISL.Formulas]
+BoxR [constructor, in ISL.Sequents]
+

C

+conjunction [definition, in ISL.Environments]
+conjunction_L [lemma, in ISL.SequentProps]
+conjunction_R2 [lemma, in ISL.SequentProps]
+conjunction_R1 [lemma, in ISL.SequentProps]
+contraction [lemma, in ISL.SequentProps]
+CountablyManyFormulas [section, in ISL.Formulas]
+

D

+decide_in [lemma, in ISL.Environments]
+difference_include [lemma, in ISL.Environments]
+difference_singleton [lemma, in ISL.Environments]
+diff_not_in [lemma, in ISL.Environments]
+disjunction [definition, in ISL.Environments]
+disjunction_R [lemma, in ISL.SequentProps]
+disjunction_L [lemma, in ISL.SequentProps]
+

E

+E [definition, in ISL.PropQuantifiers]
+EA [definition, in ISL.PropQuantifiers]
+EA_vars [lemma, in ISL.PropQuantifiers]
+EA_eq [lemma, in ISL.PropQuantifiers]
+Ef [definition, in ISL.PropQuantifiers]
+elem_of_open_boxes [lemma, in ISL.Environments]
+entail_correct [lemma, in ISL.PropQuantifiers]
+env [definition, in ISL.Environments]
+Environments [library]
+EnvMS [module, in ISL.Environments]
+EnvMS.diff [definition, in ISL.Environments]
+EnvMS.diff_mult [lemma, in ISL.Environments]
+EnvMS.empty [definition, in ISL.Environments]
+EnvMS.empty_mult [lemma, in ISL.Environments]
+EnvMS.gmultiset_choose_or_empty [lemma, in ISL.Environments]
+EnvMS.intersection [definition, in ISL.Environments]
+EnvMS.intersection_mult [lemma, in ISL.Environments]
+EnvMS.meq [definition, in ISL.Environments]
+EnvMS.meq_multeq [lemma, in ISL.Environments]
+EnvMS.mset_ind_type [definition, in ISL.Environments]
+EnvMS.mult [definition, in ISL.Environments]
+EnvMS.multeq_meq [lemma, in ISL.Environments]
+EnvMS.Multiset [definition, in ISL.Environments]
+EnvMS.mult_eqA_compat [lemma, in ISL.Environments]
+EnvMS.Sid [module, in ISL.Environments]
+EnvMS.Sid.Dom [module, in ISL.Environments]
+EnvMS.Sid.Dom.A [definition, in ISL.Environments]
+EnvMS.Sid.Eq [module, in ISL.Environments]
+EnvMS.Sid.eqA_dec [definition, in ISL.Environments]
+EnvMS.singleton [definition, in ISL.Environments]
+EnvMS.singleton_mult_notin [lemma, in ISL.Environments]
+EnvMS.singleton_mult_in [lemma, in ISL.Environments]
+EnvMS.union [definition, in ISL.Environments]
+EnvMS.union_mult [lemma, in ISL.Environments]
+env_order_eq_add [lemma, in ISL.Order]
+env_order_cancel_right [lemma, in ISL.Order]
+env_order_4 [lemma, in ISL.Order]
+env_order_3 [lemma, in ISL.Order]
+env_order_2 [lemma, in ISL.Order]
+env_order_0 [lemma, in ISL.Order]
+env_order_disj_union_compat_strong_right [lemma, in ISL.Order]
+env_order_disj_union_compat [lemma, in ISL.Order]
+env_order_disj_union_compat_right [lemma, in ISL.Order]
+env_order_disj_union_compat_left [lemma, in ISL.Order]
+env_order_add_compat [lemma, in ISL.Order]
+env_order_compat [lemma, in ISL.Order]
+env_order_1 [lemma, in ISL.Order]
+env_order_equiv_left_compat [lemma, in ISL.Order]
+env_order_equiv_right_compat [lemma, in ISL.Order]
+env_order_trans [instance, in ISL.Order]
+env_order [definition, in ISL.Order]
+env_equiv_eq [lemma, in ISL.Environments]
+env_add_inv' [lemma, in ISL.Environments]
+env_add_inv [lemma, in ISL.Environments]
+env_add_comm [lemma, in ISL.Environments]
+env_in_add [lemma, in ISL.Environments]
+env_replace [lemma, in ISL.Environments]
+equiv_assoc [instance, in ISL.Environments]
+equiv_disj_union_compat_r [lemma, in ISL.Environments]
+exfalso [lemma, in ISL.SequentProps]
+ExFalso [constructor, in ISL.Sequents]
+E_of_empty [lemma, in ISL.PropQuantifiers]
+E_left [lemma, in ISL.PropQuantifiers]
+E_irr [lemma, in ISL.PropQuantifiers]
+e_rule_vars [lemma, in ISL.PropQuantifiers]
+E_eq [definition, in ISL.PropQuantifiers]
+e_rule_cong [lemma, in ISL.PropQuantifiers]
+e_rule [definition, in ISL.PropQuantifiers]
+

F

+fomula_bottom [instance, in ISL.Formulas]
+form [inductive, in ISL.Formulas]
+Formulas [library]
+form_order [definition, in ISL.Formulas]
+form_count [instance, in ISL.Formulas]
+form_to_gen_tree [definition, in ISL.Formulas]
+form_eq_dec [instance, in ISL.Formulas]
+form_top [instance, in ISL.Formulas]
+

G

+generalised_contraction [lemma, in ISL.SequentProps]
+generalised_axiom [lemma, in ISL.SequentProps]
+generalised_weakeningR [lemma, in ISL.SequentProps]
+generalised_weakeningL [lemma, in ISL.SequentProps]
+gen_tree_to_form [definition, in ISL.Formulas]
+gmultiset_rec [lemma, in ISL.Environments]
+

H

+height [definition, in ISL.SequentProps]
+height_0 [lemma, in ISL.SequentProps]
+

I

+ImpBox [constructor, in ISL.Sequents]
+ImpBox_dup [lemma, in ISL.SequentProps]
+ImpL [lemma, in ISL.SequentProps]
+ImpLAnd [constructor, in ISL.Sequents]
+ImpLAnd_rev [lemma, in ISL.SequentProps]
+ImpLBox_prev [lemma, in ISL.SequentProps]
+Implies [constructor, in ISL.Formulas]
+ImpLImp [constructor, in ISL.Sequents]
+ImpLImp_dup [lemma, in ISL.SequentProps]
+ImpLImp_prev [lemma, in ISL.SequentProps]
+ImpLOr [constructor, in ISL.Sequents]
+ImpLOr_rev [lemma, in ISL.SequentProps]
+ImpLVar [constructor, in ISL.Sequents]
+ImpLVar_rev [lemma, in ISL.SequentProps]
+ImpR [constructor, in ISL.Sequents]
+ImpR_rev [lemma, in ISL.SequentProps]
+imp_cut [lemma, in ISL.SequentProps]
+In_open_boxes [lemma, in ISL.Environments]
+in_difference [lemma, in ISL.Environments]
+in_map_ext [lemma, in ISL.Environments]
+in_map_empty [lemma, in ISL.Environments]
+in_map_in [lemma, in ISL.Environments]
+in_subset [definition, in ISL.Environments]
+in_in_map [lemma, in ISL.Environments]
+in_map [definition, in ISL.Environments]
+in_map_aux [definition, in ISL.Environments]
+irreducible [definition, in ISL.Environments]
+irreflexive_form_order [instance, in ISL.Formulas]
+is_box_weight_open_box [lemma, in ISL.SequentProps]
+is_not_box_open_box [lemma, in ISL.Environments]
+is_box [definition, in ISL.Environments]
+

M

+make_disj_complete_R [lemma, in ISL.SequentProps]
+make_disj_sound_R [lemma, in ISL.SequentProps]
+make_conj_complete_R [lemma, in ISL.SequentProps]
+make_conj_sound_R [lemma, in ISL.SequentProps]
+make_conj_complete_L [lemma, in ISL.SequentProps]
+make_conj_sound_L [lemma, in ISL.SequentProps]
+make_disj_complete [lemma, in ISL.SequentProps]
+make_disj_sound_L [lemma, in ISL.SequentProps]
+make_impl_sound_R [lemma, in ISL.SequentProps]
+make_impl_complete_R [lemma, in ISL.SequentProps]
+make_impl_complete_L2 [lemma, in ISL.SequentProps]
+make_impl_complete_L [lemma, in ISL.SequentProps]
+make_impl_sound_L2' [lemma, in ISL.SequentProps]
+make_impl_sound_L2 [lemma, in ISL.SequentProps]
+make_impl_sound_L [lemma, in ISL.SequentProps]
+make_impl_weight2 [lemma, in ISL.Order]
+make_impl_weight [lemma, in ISL.Order]
+make_impl_spec [lemma, in ISL.Environments]
+make_impl [definition, in ISL.Environments]
+make_disj_spec [lemma, in ISL.Environments]
+make_disj [definition, in ISL.Environments]
+make_conj_spec [lemma, in ISL.Environments]
+make_conj [definition, in ISL.Environments]
+MO [module, in ISL.Environments]
+

O

+occurs_in [definition, in ISL.Formulas]
+occurs_in_open_boxes [lemma, in ISL.Environments]
+occurs_in_make_impl2 [lemma, in ISL.Environments]
+occurs_in_make_impl [lemma, in ISL.Environments]
+occurs_in_make_disj [lemma, in ISL.Environments]
+occurs_in_make_conj [lemma, in ISL.Environments]
+openboxes_env_order [lemma, in ISL.Order]
+open_box_L [lemma, in ISL.SequentProps]
+open_boxes_case [lemma, in ISL.PropQuantifiers]
+open_boxes_env_order [lemma, in ISL.Order]
+open_boxes_spec' [lemma, in ISL.Environments]
+open_boxes_spec [lemma, in ISL.Environments]
+open_boxes_remove [lemma, in ISL.Environments]
+open_boxes_equiv [instance, in ISL.Environments]
+open_boxes_add [lemma, in ISL.Environments]
+open_boxes_singleton [lemma, in ISL.Environments]
+open_boxes_disj_union [lemma, in ISL.Environments]
+open_boxes_empty [lemma, in ISL.Environments]
+open_boxes [definition, in ISL.Environments]
+open_box [definition, in ISL.Environments]
+Or [constructor, in ISL.Formulas]
+Order [library]
+OrL [constructor, in ISL.Sequents]
+OrL_rev [lemma, in ISL.SequentProps]
+OrR_idemp [lemma, in ISL.SequentProps]
+OrR1 [constructor, in ISL.Sequents]
+OrR1Bot_rev [lemma, in ISL.SequentProps]
+OrR2 [constructor, in ISL.Sequents]
+OrR2Bot_rev [lemma, in ISL.SequentProps]
+

P

+pitts [lemma, in ISL.PropQuantifiers]
+Pitts [section, in ISL.PropQuantifiers]
+Pitts.Correctness [section, in ISL.PropQuantifiers]
+Pitts.Correctness.EntailmentCorrect [section, in ISL.PropQuantifiers]
+Pitts.Correctness.PropQuantCorrect [section, in ISL.PropQuantifiers]
+Pitts.Correctness.VariablesCorrect [section, in ISL.PropQuantifiers]
+Pitts.p [variable, in ISL.PropQuantifiers]
+Pitts.PropQuantDefinition [section, in ISL.PropQuantifiers]
+pointed_env_order [definition, in ISL.Order]
+pointed_env [definition, in ISL.Order]
+pq_correct [lemma, in ISL.PropQuantifiers]
+Proper_env_order [instance, in ISL.Order]
+proper_Provable [instance, in ISL.Sequents]
+proper_open_boxes [instance, in ISL.Environments]
+proper_disj_union [instance, in ISL.Environments]
+proper_elem_of [instance, in ISL.Environments]
+PropQuantifiers [library]
+Provable [inductive, in ISL.Sequents]
+p_contr [lemma, in ISL.SequentProps]
+

S

+SequentProps [library]
+Sequents [library]
+singleton [instance, in ISL.Environments]
+singletonMS [instance, in ISL.Environments]
+strongness [lemma, in ISL.SequentProps]
+SubAnd [constructor, in ISL.Formulas]
+SubBox [constructor, in ISL.Formulas]
+SubEq [constructor, in ISL.Formulas]
+subform [inductive, in ISL.Formulas]
+SubImpl [constructor, in ISL.Formulas]
+SubOr [constructor, in ISL.Formulas]
+

T

+TopL_rev [lemma, in ISL.SequentProps]
+transitive_form_order [instance, in ISL.Formulas]
+

U

+union_difference_R [lemma, in ISL.Environments]
+union_difference_L [lemma, in ISL.Environments]
+

V

+Var [constructor, in ISL.Formulas]
+variable [definition, in ISL.Formulas]
+variables_disjunction [lemma, in ISL.Environments]
+variables_conjunction [lemma, in ISL.Environments]
+vars_incl [definition, in ISL.PropQuantifiers]
+var_not_in_env [definition, in ISL.Environments]
+

W

+weakening [lemma, in ISL.SequentProps]
+weak_ImpL [lemma, in ISL.SequentProps]
+weight [definition, in ISL.Formulas]
+weight_open_box [lemma, in ISL.SequentProps]
+weight_ind [definition, in ISL.Formulas]
+weight_pos [lemma, in ISL.Formulas]
+wf_pointed_order [lemma, in ISL.Order]
+wf_env_order [definition, in ISL.Order]
+

other

+_ ≺· _ [notation, in ISL.Order]
+_ ≼ _ [notation, in ISL.Order]
+_ ≺ _ [notation, in ISL.Order]
+_ ⊢ _ [notation, in ISL.Sequents]
+_ ≺f _ [notation, in ISL.Formulas]
+_ _ ⇔ _ _ [notation, in ISL.Formulas]
+_ → _ [notation, in ISL.Formulas]
+_ ∨ _ [notation, in ISL.Formulas]
+_ ∧ _ [notation, in ISL.Formulas]
+_ ⇢ _ [notation, in ISL.Environments]
+_ ⊻ _ [notation, in ISL.Environments]
+_ ⊼ _ [notation, in ISL.Environments]
+_ • _ [notation, in ISL.Environments]
+¬ _ [notation, in ISL.Formulas]
+⊗ _ [notation, in ISL.Environments]
+⊙ _ [notation, in ISL.Environments]
+⊤ [notation, in ISL.Formulas]
+⊥ [notation, in ISL.Formulas]
+⋀ [notation, in ISL.Environments]
+⋁ [notation, in ISL.Environments]
+□ _ [notation, in ISL.Formulas]
+

+

Notation Index

+

other

+_ ≺· _ [in ISL.Order]
+_ ≼ _ [in ISL.Order]
+_ ≺ _ [in ISL.Order]
+_ ⊢ _ [in ISL.Sequents]
+_ ≺f _ [in ISL.Formulas]
+_ _ ⇔ _ _ [in ISL.Formulas]
+_ → _ [in ISL.Formulas]
+_ ∨ _ [in ISL.Formulas]
+_ ∧ _ [in ISL.Formulas]
+_ ⇢ _ [in ISL.Environments]
+_ ⊻ _ [in ISL.Environments]
+_ ⊼ _ [in ISL.Environments]
+_ • _ [in ISL.Environments]
+¬ _ [in ISL.Formulas]
+⊗ _ [in ISL.Environments]
+⊙ _ [in ISL.Environments]
+⊤ [in ISL.Formulas]
+⊥ [in ISL.Formulas]
+⋀ [in ISL.Environments]
+⋁ [in ISL.Environments]
+□ _ [in ISL.Formulas]
+

+

Module Index

+

E

+EnvMS [in ISL.Environments]
+EnvMS.Sid [in ISL.Environments]
+EnvMS.Sid.Dom [in ISL.Environments]
+EnvMS.Sid.Eq [in ISL.Environments]
+

M

+MO [in ISL.Environments]
+

+

Variable Index

+

P

+Pitts.p [in ISL.PropQuantifiers]
+

+

Library Index

+

E

+Environments
+

F

+Formulas
+

O

+Order
+

P

+PropQuantifiers
+

S

+SequentProps
+Sequents
+

+

Lemma Index

+

A

+AndL_rev [in ISL.SequentProps]
+AndR_rev [in ISL.SequentProps]
+A_right [in ISL.PropQuantifiers]
+a_rule_env_spec [in ISL.PropQuantifiers]
+a_rule_form_vars [in ISL.PropQuantifiers]
+a_rule_env_vars [in ISL.PropQuantifiers]
+a_rule_form_cong [in ISL.PropQuantifiers]
+a_rule_env_cong [in ISL.PropQuantifiers]
+

C

+conjunction_L [in ISL.SequentProps]
+conjunction_R2 [in ISL.SequentProps]
+conjunction_R1 [in ISL.SequentProps]
+contraction [in ISL.SequentProps]
+

D

+decide_in [in ISL.Environments]
+difference_include [in ISL.Environments]
+difference_singleton [in ISL.Environments]
+diff_not_in [in ISL.Environments]
+disjunction_R [in ISL.SequentProps]
+disjunction_L [in ISL.SequentProps]
+

E

+EA_vars [in ISL.PropQuantifiers]
+EA_eq [in ISL.PropQuantifiers]
+elem_of_open_boxes [in ISL.Environments]
+entail_correct [in ISL.PropQuantifiers]
+EnvMS.diff_mult [in ISL.Environments]
+EnvMS.empty_mult [in ISL.Environments]
+EnvMS.gmultiset_choose_or_empty [in ISL.Environments]
+EnvMS.intersection_mult [in ISL.Environments]
+EnvMS.meq_multeq [in ISL.Environments]
+EnvMS.multeq_meq [in ISL.Environments]
+EnvMS.mult_eqA_compat [in ISL.Environments]
+EnvMS.singleton_mult_notin [in ISL.Environments]
+EnvMS.singleton_mult_in [in ISL.Environments]
+EnvMS.union_mult [in ISL.Environments]
+env_order_eq_add [in ISL.Order]
+env_order_cancel_right [in ISL.Order]
+env_order_4 [in ISL.Order]
+env_order_3 [in ISL.Order]
+env_order_2 [in ISL.Order]
+env_order_0 [in ISL.Order]
+env_order_disj_union_compat_strong_right [in ISL.Order]
+env_order_disj_union_compat [in ISL.Order]
+env_order_disj_union_compat_right [in ISL.Order]
+env_order_disj_union_compat_left [in ISL.Order]
+env_order_add_compat [in ISL.Order]
+env_order_compat [in ISL.Order]
+env_order_1 [in ISL.Order]
+env_order_equiv_left_compat [in ISL.Order]
+env_order_equiv_right_compat [in ISL.Order]
+env_equiv_eq [in ISL.Environments]
+env_add_inv' [in ISL.Environments]
+env_add_inv [in ISL.Environments]
+env_add_comm [in ISL.Environments]
+env_in_add [in ISL.Environments]
+env_replace [in ISL.Environments]
+equiv_disj_union_compat_r [in ISL.Environments]
+exfalso [in ISL.SequentProps]
+E_of_empty [in ISL.PropQuantifiers]
+E_left [in ISL.PropQuantifiers]
+E_irr [in ISL.PropQuantifiers]
+e_rule_vars [in ISL.PropQuantifiers]
+e_rule_cong [in ISL.PropQuantifiers]
+

G

+generalised_contraction [in ISL.SequentProps]
+generalised_axiom [in ISL.SequentProps]
+generalised_weakeningR [in ISL.SequentProps]
+generalised_weakeningL [in ISL.SequentProps]
+gmultiset_rec [in ISL.Environments]
+

H

+height_0 [in ISL.SequentProps]
+

I

+ImpBox_dup [in ISL.SequentProps]
+ImpL [in ISL.SequentProps]
+ImpLAnd_rev [in ISL.SequentProps]
+ImpLBox_prev [in ISL.SequentProps]
+ImpLImp_dup [in ISL.SequentProps]
+ImpLImp_prev [in ISL.SequentProps]
+ImpLOr_rev [in ISL.SequentProps]
+ImpLVar_rev [in ISL.SequentProps]
+ImpR_rev [in ISL.SequentProps]
+imp_cut [in ISL.SequentProps]
+In_open_boxes [in ISL.Environments]
+in_difference [in ISL.Environments]
+in_map_ext [in ISL.Environments]
+in_map_empty [in ISL.Environments]
+in_map_in [in ISL.Environments]
+in_in_map [in ISL.Environments]
+is_box_weight_open_box [in ISL.SequentProps]
+is_not_box_open_box [in ISL.Environments]
+

M

+make_disj_complete_R [in ISL.SequentProps]
+make_disj_sound_R [in ISL.SequentProps]
+make_conj_complete_R [in ISL.SequentProps]
+make_conj_sound_R [in ISL.SequentProps]
+make_conj_complete_L [in ISL.SequentProps]
+make_conj_sound_L [in ISL.SequentProps]
+make_disj_complete [in ISL.SequentProps]
+make_disj_sound_L [in ISL.SequentProps]
+make_impl_sound_R [in ISL.SequentProps]
+make_impl_complete_R [in ISL.SequentProps]
+make_impl_complete_L2 [in ISL.SequentProps]
+make_impl_complete_L [in ISL.SequentProps]
+make_impl_sound_L2' [in ISL.SequentProps]
+make_impl_sound_L2 [in ISL.SequentProps]
+make_impl_sound_L [in ISL.SequentProps]
+make_impl_weight2 [in ISL.Order]
+make_impl_weight [in ISL.Order]
+make_impl_spec [in ISL.Environments]
+make_disj_spec [in ISL.Environments]
+make_conj_spec [in ISL.Environments]
+

O

+occurs_in_open_boxes [in ISL.Environments]
+occurs_in_make_impl2 [in ISL.Environments]
+occurs_in_make_impl [in ISL.Environments]
+occurs_in_make_disj [in ISL.Environments]
+occurs_in_make_conj [in ISL.Environments]
+openboxes_env_order [in ISL.Order]
+open_box_L [in ISL.SequentProps]
+open_boxes_case [in ISL.PropQuantifiers]
+open_boxes_env_order [in ISL.Order]
+open_boxes_spec' [in ISL.Environments]
+open_boxes_spec [in ISL.Environments]
+open_boxes_remove [in ISL.Environments]
+open_boxes_add [in ISL.Environments]
+open_boxes_singleton [in ISL.Environments]
+open_boxes_disj_union [in ISL.Environments]
+open_boxes_empty [in ISL.Environments]
+OrL_rev [in ISL.SequentProps]
+OrR_idemp [in ISL.SequentProps]
+OrR1Bot_rev [in ISL.SequentProps]
+OrR2Bot_rev [in ISL.SequentProps]
+

P

+pitts [in ISL.PropQuantifiers]
+pq_correct [in ISL.PropQuantifiers]
+p_contr [in ISL.SequentProps]
+

S

+strongness [in ISL.SequentProps]
+

T

+TopL_rev [in ISL.SequentProps]
+

U

+union_difference_R [in ISL.Environments]
+union_difference_L [in ISL.Environments]
+

V

+variables_disjunction [in ISL.Environments]
+variables_conjunction [in ISL.Environments]
+

W

+weakening [in ISL.SequentProps]
+weak_ImpL [in ISL.SequentProps]
+weight_open_box [in ISL.SequentProps]
+weight_pos [in ISL.Formulas]
+wf_pointed_order [in ISL.Order]
+

+

Constructor Index

+

A

+And [in ISL.Formulas]
+AndL [in ISL.Sequents]
+AndR [in ISL.Sequents]
+Atom [in ISL.Sequents]
+

B

+Bot [in ISL.Formulas]
+Box [in ISL.Formulas]
+BoxR [in ISL.Sequents]
+

E

+ExFalso [in ISL.Sequents]
+

I

+ImpBox [in ISL.Sequents]
+ImpLAnd [in ISL.Sequents]
+Implies [in ISL.Formulas]
+ImpLImp [in ISL.Sequents]
+ImpLOr [in ISL.Sequents]
+ImpLVar [in ISL.Sequents]
+ImpR [in ISL.Sequents]
+

O

+Or [in ISL.Formulas]
+OrL [in ISL.Sequents]
+OrR1 [in ISL.Sequents]
+OrR2 [in ISL.Sequents]
+

S

+SubAnd [in ISL.Formulas]
+SubBox [in ISL.Formulas]
+SubEq [in ISL.Formulas]
+SubImpl [in ISL.Formulas]
+SubOr [in ISL.Formulas]
+

V

+Var [in ISL.Formulas]
+

+

Inductive Index

+

F

+form [in ISL.Formulas]
+

P

+Provable [in ISL.Sequents]
+

S

+subform [in ISL.Formulas]
+

+

Section Index

+

C

+CountablyManyFormulas [in ISL.Formulas]
+

P

+Pitts [in ISL.PropQuantifiers]
+Pitts.Correctness [in ISL.PropQuantifiers]
+Pitts.Correctness.EntailmentCorrect [in ISL.PropQuantifiers]
+Pitts.Correctness.PropQuantCorrect [in ISL.PropQuantifiers]
+Pitts.Correctness.VariablesCorrect [in ISL.PropQuantifiers]
+Pitts.PropQuantDefinition [in ISL.PropQuantifiers]
+

+

Instance Index

+

A

+assoc_meq_union [in ISL.Order]
+

E

+env_order_trans [in ISL.Order]
+equiv_assoc [in ISL.Environments]
+

F

+fomula_bottom [in ISL.Formulas]
+form_count [in ISL.Formulas]
+form_eq_dec [in ISL.Formulas]
+form_top [in ISL.Formulas]
+

I

+irreflexive_form_order [in ISL.Formulas]
+

O

+open_boxes_equiv [in ISL.Environments]
+

P

+Proper_env_order [in ISL.Order]
+proper_Provable [in ISL.Sequents]
+proper_open_boxes [in ISL.Environments]
+proper_disj_union [in ISL.Environments]
+proper_elem_of [in ISL.Environments]
+

S

+singleton [in ISL.Environments]
+singletonMS [in ISL.Environments]
+

T

+transitive_form_order [in ISL.Formulas]
+

+

Definition Index

+

A

+A [in ISL.PropQuantifiers]
+Af [in ISL.PropQuantifiers]
+A_eq [in ISL.PropQuantifiers]
+a_rule_form [in ISL.PropQuantifiers]
+a_rule_env [in ISL.PropQuantifiers]
+

C

+conjunction [in ISL.Environments]
+

D

+disjunction [in ISL.Environments]
+

E

+E [in ISL.PropQuantifiers]
+EA [in ISL.PropQuantifiers]
+Ef [in ISL.PropQuantifiers]
+env [in ISL.Environments]
+EnvMS.diff [in ISL.Environments]
+EnvMS.empty [in ISL.Environments]
+EnvMS.intersection [in ISL.Environments]
+EnvMS.meq [in ISL.Environments]
+EnvMS.mset_ind_type [in ISL.Environments]
+EnvMS.mult [in ISL.Environments]
+EnvMS.Multiset [in ISL.Environments]
+EnvMS.Sid.Dom.A [in ISL.Environments]
+EnvMS.Sid.eqA_dec [in ISL.Environments]
+EnvMS.singleton [in ISL.Environments]
+EnvMS.union [in ISL.Environments]
+env_order [in ISL.Order]
+E_eq [in ISL.PropQuantifiers]
+e_rule [in ISL.PropQuantifiers]
+

F

+form_order [in ISL.Formulas]
+form_to_gen_tree [in ISL.Formulas]
+

G

+gen_tree_to_form [in ISL.Formulas]
+

H

+height [in ISL.SequentProps]
+

I

+in_subset [in ISL.Environments]
+in_map [in ISL.Environments]
+in_map_aux [in ISL.Environments]
+irreducible [in ISL.Environments]
+is_box [in ISL.Environments]
+

M

+make_impl [in ISL.Environments]
+make_disj [in ISL.Environments]
+make_conj [in ISL.Environments]
+

O

+occurs_in [in ISL.Formulas]
+open_boxes [in ISL.Environments]
+open_box [in ISL.Environments]
+

P

+pointed_env_order [in ISL.Order]
+pointed_env [in ISL.Order]
+

V

+variable [in ISL.Formulas]
+vars_incl [in ISL.PropQuantifiers]
+var_not_in_env [in ISL.Environments]
+

W

+weight [in ISL.Formulas]
+weight_ind [in ISL.Formulas]
+wf_env_order [in ISL.Order]
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(271 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(21 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(5 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(138 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(25 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(7 entries)
Instance IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(17 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(48 entries)
+
+ +
+ + + diff --git a/html/toc.html b/html/toc.html new file mode 100644 index 0000000..fbd528f --- /dev/null +++ b/html/toc.html @@ -0,0 +1,156 @@ + + + + + + + + + + + + + +
+ + +
+ + +