Require Import List Permutation Arith.
From Undecidability.ILL Require Import ILL CLL ill_cll.
Set Implicit Arguments.
Fact app_eq_single_inv X (l m : list X) x :
l++m = x::nil
-> l = nil /\ m = x::nil
\/ l = x::nil /\ m = nil.
Proof.
intros H.
destruct l as [ | y l ]; auto.
right.
inversion H.
destruct l; destruct m; auto; discriminate.
Qed.
Tactic Notation "app" "inv" "singleton" "in" hyp(H) :=
apply app_eq_single_inv in H as [ (-> & ->) | (-> & ->) ].
Tactic Notation "app" "inv" "nil" "in" hyp(H) :=
apply app_eq_nil in H as (-> & ->).
Local Infix "~p" := (@Permutation _) (at level 70).
Section S_ill_cll_restr.
Notation "Γ '⊢i' A" := (S_ill_restr Γ A) (at level 70).
Notation "Γ '⊢c' Δ" := (S_cll_restr Γ Δ) (at level 70).
Hint Resolve Permutation_map : core.
Theorem S_ill_cll_restr Γ A : Γ ⊢i A -> ⟦Γ⟧ ⊢c [A]::∅.
Proof.
induction 1.
+ apply in_cll1_ax.
+ apply (@in_cll1_perm ⟦Γ⟧ ([A]::nil)); auto.
+ simpl; rewrite map_app; now apply in_cll1_limp_l with (Δ := ∅) (Δ' := _::_).
+ now apply in_cll1_limp_r with (Δ := ∅).
+ now apply in_cll1_with_l1.
+ now apply in_cll1_with_l2.
+ now apply in_cll1_with_r with (Δ := ∅).
+ now apply in_cll1_bang_l.
+ rewrite ill_cll_lbang in *; simpl; now apply in_cll1_bang_r.
+ now apply in_cll1_weak_l.
+ now apply in_cll1_cntr_l.
Qed.
Let cll_ill_empty_rec Γ Δ : Γ ⊢c Δ -> Δ <> ∅.
Proof.
induction 1 as [ A
| Γ Δ Γ' Δ' H1 H2 H3 IH3
| Γ Δ Γ' Δ' A B H1 IH1 H2 IH2 | Γ Δ A B H1 IH1
| Γ Δ A B H1 IH1 | Γ Δ A B H1 IH1 | Γ Δ A B H1 IH1 H2 IH2
| Γ A Δ H1 IH1 | Γ A H1 IH1
| Γ A Δ H1 IH1
| Γ A Δ H1 IH1 ];
auto; try discriminate.
+ intros ->; now apply IH3, Permutation_nil, Permutation_sym.
+ intros H; now app inv nil in H.
Qed.
Let cll_ill_empty Γ : ~ Γ ⊢c ∅.
Proof. intros H; now apply cll_ill_empty_rec with (1 := H). Qed.
Let cll_ill_rec Γ Δ : Γ ⊢c Δ -> forall A, Δ = A::∅ -> ⟪Γ⟫ ⊢i ⟨A⟩.
Proof.
induction 1 as [ A
| Γ Δ Γ' Δ' H1 H2 H3 IH3
| Γ Δ Γ' Δ' A B H1 IH1 H2 IH2 | Γ Δ A B H1 IH1
| Γ Δ A B H1 IH1 | Γ Δ A B H1 IH1 | Γ Δ A B H1 IH1 H2 IH2
| Γ A Δ H1 IH1 | Γ A H1 IH1
| Γ A Δ H1 IH1
| Γ A Δ H1 IH1 ];
intros C HC; try discriminate.
+ inversion HC; constructor.
+ subst.
apply (Permutation_map cll_ill) in H1.
constructor 2 with (1 := H1).
apply Permutation_sym, Permutation_length_1_inv in H2 as ->.
apply IH3; auto.
+ app inv singleton in HC.
* simpl; rewrite map_app; constructor; auto.
* apply cll_ill_empty in H2 as [].
+ inversion HC; subst.
constructor; apply IH1; auto.
+ rewrite HC in *.
apply in_ill1_with_l1, IH1; auto.
+ rewrite HC in *.
apply in_ill1_with_l2, IH1; auto.
+ inversion HC; subst; clear HC.
constructor; auto.
+ subst; constructor; apply IH1; auto.
+ inversion HC; subst.
rewrite cll_ill_lbang; simpl.
constructor.
rewrite <- cll_ill_lbang; auto.
+ subst; apply in_ill1_weak; auto.
+ subst; apply in_ill1_cntr; auto.
Qed.
Theorem S_cll_ill_restr Γ A : Γ ⊢c A::∅ -> ⟪Γ⟫ ⊢i ⟨A⟩.
Proof.
intros H; now apply cll_ill_rec with (1 := H).
Qed.
Hint Resolve S_ill_cll_restr S_cll_ill_restr : core.
Theorem S_ill_cll_restr_equiv Γ A : Γ ⊢i A <-> ⟦Γ⟧ ⊢c [A]::∅.
Proof.
split; auto.
intros H; apply S_cll_ill_restr in H; revert H.
now rewrite ill_cll_ill_list, ill_cll_ill.
Qed.
End S_ill_cll_restr.