Click on a command or tactic to see a detailed view of its use.

Kind atm type.

Type a, b, c, d, e, f atm.

%% We reuse the o type to define LL formulas
Type atom, natom   atm -> o.
Type tens, par     o -> o -> o.
Type one, bot      o.

Define is_fm : o -> prop by
; is_fm (atom A)
; is_fm (natom A)
; is_fm (tens A B) := is_fm A /\ is_fm B
; is_fm (par A B) := is_fm A /\ is_fm B
; is_fm one
; is_fm bot
.

Define dual : o -> o -> prop by
; dual (atom A) (natom A)
; dual (tens A B) (par AA BB) := dual A AA /\ dual B BB
; dual one bot
.

Theorem dual_is : forall A B, dual A B -> is_fm A /\ is_fm B.
induction on 1. intros. case H1.
  search.
  apply IH to *H2. apply IH to *H3. search.
  search.
Import "../../lib/merge" with is_o := is_fm. [View ../../lib/merge]

Define mll : olist -> prop by
; mll L :=
    exists A, adj (natom A :: nil) (atom A) L

; mll L :=
    exists A B LL JJ KK J K,
      adj LL (tens A B) L /\
      merge JJ KK LL /\
      adj JJ A J /\ mll J /\
      adj KK B K /\ mll K

; mll (one :: nil)

; mll L :=
    exists A B LL J K,
      adj LL (par A B) L /\
      adj LL A J /\
      adj J B K /\
      mll K

; mll L :=
    exists LL,
      adj LL bot L /\
      mll LL
.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Theorem generalized_id : forall A B, dual A B -> mll (A :: B :: nil).
induction on 1. intros. case H1.
  search.
  apply IH to H2. apply IH to H3.
   apply dual_is to H2. apply dual_is to H3.
   unfold 4. witness AA. witness BB. witness tens A1 B1 :: nil.
   witness tens A1 B1 :: AA :: nil.
   witness tens A1 B1 :: AA :: BB :: nil.
   split. search. search. search.
   unfold 2. witness A1. witness B1.
   witness AA :: BB :: nil.
   witness AA :: nil. witness BB :: nil.
   witness A1 :: AA :: nil. witness B1 :: BB :: nil.
   search.
  search.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Theorem mll_perm : forall K L,
  mll K -> perm K L -> mll L.
induction on 1. intros. case H1.
  case H3.
    apply perm_cons_1 to *H2.
     apply perm_cons_1 to *H7. case H9. case H8. search. case H10.
    apply perm_cons_1 to *H2. apply adj_nil_1 to *H5.
     apply perm_cons_1 to *H7. apply adj_swap to *H8 *H6.
     apply perm_nil_1 to *H9. apply adj_nil_1 to *H10.
     unfold 1. search.

  apply adj_2_is_o to H5. apply adj_1_is_list to H5.
   apply adj_2_is_o to H7. apply adj_1_is_list to H7.
   assert perm J (A :: JJ).
     apply perm_refl to H10. search.
   assert perm K1 (B :: KK).
     apply perm_refl to H12. search.
   apply IH to *H6 *H13.
   apply IH to *H8 *H14.
   apply adj_perm_full to H2 H3. apply perm_merge_3 to *H4 *H18.
   unfold 2. search.

  case H2. case H3.
    apply perm_nil_1 to *H5. apply adj_nil_1 to *H4. search.
    case H7.

  apply adj_perm_full to *H2 *H3.
   assert perm J (A :: KK).
     apply adj_1_is_list to H7. apply adj_2_is_o to H4. search.
   assert perm K1 (B :: A :: KK).
     apply adj_1_is_list to H7. apply adj_2_is_o to H4. apply adj_2_is_o to H5.
      search.
   apply IH to *H6 *H10.
   apply adj_1_is_list to H7. apply adj_2_is_o to H4. apply adj_2_is_o to H5.
   unfold 4. search.

  apply adj_perm_full to *H2 *H3.
   apply IH to *H4 *H6.
   unfold 5. search.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Inversion theorems

Theorem bot_inv : forall J L,
  mll L -> adj J bot L -> mll J.
induction on 1. intros. case H1.
  apply adj_same_result_diff to H2 H3. case H4.
   case H5. case H7.

  apply adj_same_result_diff to H2 H3. case H9.
   apply merge_unadj_3 to H4 H10. case H11.
    apply adj_swap to H12 H5. apply IH to *H6 H15.
     apply merge_unadj_1 to H4 H12.
     apply adj_swap to H17 H3.
     assert mll U1. apply adj_same_result to H20 H2. backchain mll_perm with K = U1.

    apply merge_unadj_2 to *H4 H12. apply adj_same_result to H14 H10.
     apply perm_merge_3 to *H15 *H16.
     apply adj_swap to H12 H7. apply IH to *H8 H19.
     apply adj_swap to H10 H3. assert mll U1.
     apply adj_same_result to H22 H2. backchain mll_perm with K = U1.

  case H2. case H4.

  apply adj_same_result_diff to H2 H3. case H7.
   apply adj_swap to H8 H4.  apply adj_swap to H10 H5.
   apply IH to *H6 H12.
   apply adj_swap to H8 H3. assert mll U2.
   apply adj_same_result to H15 H2. backchain mll_perm with K = U2.

  apply adj_same_result to H3 H2. backchain mll_perm.
Theorem adj_sequence : forall J A K B L,
  adj J A K ->
  adj J B L ->
  exists KK LL, adj L A LL /\ adj K B KK /\ perm KK LL.
induction on 1. intros. case H1.
  apply adj_3_is_list to H2. apply adj_exists to H3 H5.
   witness A :: L. witness M. split. search. search.
   apply adj_3_is_list to H6. apply perm_refl to H5. search.

  case H2.
    case H6. apply adj_3_is_list to H4. witness B :: B1 :: L1. witness B :: B1 :: L1.
     apply perm_refl to _ with L = B :: B1 :: L1. search.

    apply IH to *H4 *H6. witness B1 :: KK. witness B1 :: LL. split. search. search.
     apply perm_1_is_list to H9. apply perm_2_is_list to H9. search.
Theorem par_inv : forall L JJ A B,
  mll L -> adj JJ (par A B) L ->
  exists KK LL, adj JJ A KK /\ adj KK B LL /\ mll LL.
induction on 1. intros. case H1.
  apply adj_same_result_diff to H2 H3. case H4.
   case H5. case H7.

  apply adj_same_result_diff to H2 H3. case H9.
  apply merge_unadj_3 to *H4 H10. case H11.
    apply adj_swap to H12 *H5. apply IH to *H6 *H15.
     apply adj_swap to *H14 *H16. apply adj_swap to *H20 *H17.
     apply adj_1_is_list to H10. apply adj_2_is_o to H19. apply adj_2_is_o to H21.
     assert merge U2 KK (A :: B :: KK1).
     apply adj_2_is_o to H3.
     assert mll (tens A1 B1 :: A :: B :: KK1).
     apply adj_swap to *H10 *H3.
     apply adj_same_result to H30 H2. apply adj_perm_full to H31 H29.
     apply adj_1_is_list to *H2.
     assert perm (tens A1 B1 :: A :: B :: KK1) (A :: B :: JJ).
     apply mll_perm to H28 H35.
     assert adj JJ A (A :: JJ).
     assert adj (A :: JJ) B (A :: B :: JJ).
     search.

    %% symmetric case
    apply adj_swap to *H12 *H7. apply IH to *H8 *H15.
     apply adj_swap to *H14 *H16. apply adj_swap to *H20 *H17.
     apply adj_1_is_list to H10. apply adj_2_is_o to H19. apply adj_2_is_o to H21.
     assert merge JJ1 U2 (A :: B :: KK1).
     apply adj_2_is_o to H3.
     assert mll (tens A1 B1 :: A :: B :: KK1).
     apply adj_swap to *H10 *H3.
     apply adj_same_result to H30 H2. apply adj_perm_full to H31 H29.
     apply adj_1_is_list to *H2.
     assert perm (tens A1 B1 :: A :: B :: KK1) (A :: B :: JJ).
     apply mll_perm to *H28 *H35.
     assert adj JJ A (A :: JJ).
     assert adj (A :: JJ) B (A :: B :: JJ).
     search.

  case H2. case H4.

  apply adj_same_result_diff to H2 H3. apply adj_2_is_o to H4. apply adj_2_is_o to H5. apply adj_1_is_list to H2.
  case H7.
    assert perm (A1 :: B1 :: JJ) K.
     apply perm_sym to *H12. apply mll_perm to *H6 *H13.
     search.

   apply adj_swap to H11 *H4. apply adj_swap to *H13 *H5. apply IH to *H6 *H15.
     apply adj_swap to *H14 *H16. apply adj_swap to *H20 *H17.
     apply adj_swap to *H12 *H19. apply adj_swap to *H24 *H21.
     apply adj_1_is_list to H26. assert mll (par A1 B1 :: U5).
     apply adj_2_is_o to H23. apply adj_2_is_o to H25.
     assert perm (par A1 B1 :: U5) (A :: B :: JJ).
       unfold. witness B. witness par A1 B1 :: U4. witness A :: JJ. split. search. search.
       unfold. witness A. witness par A1 B1 :: KK. witness JJ. split. search. search.
       apply adj_swap to *H11 *H3. apply adj_same_result to *H32 *H2.
       backchain perm_trans with K = U6.
       apply adj_1_is_list to H31.
       unfold. witness par A1 B1. witness KK. witness KK. split. search. search. backchain perm_refl.
     apply mll_perm to *H28 *H31.
     search.

  apply adj_same_result_diff to H2 H3. apply adj_2_is_o to H2. case H6. case H5.
    apply IH to *H4 H9.
    apply adj_3_is_list to H11.
    assert mll (bot :: LL1).
    apply adj_1_is_list to H2.
    assert perm (bot :: LL1) (A :: B :: JJ).
      unfold. witness B. witness bot :: KK1. witness A :: JJ. split. search. search.
      unfold. witness A. witness bot :: KK. witness JJ. split. search. search.
      apply adj_swap to *H9 *H3. apply adj_same_result to *H17 H2.
      backchain perm_trans with K = U.
      apply adj_1_is_list to H16. apply perm_refl to H19. search.
    apply mll_perm to *H14 *H16.
    search.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Theorem cut : forall A B JJ J KK K LL,
  dual A B ->
  adj JJ A J -> mll J ->
  adj KK B K -> mll K ->
  merge JJ KK LL ->
  mll LL.
induction on 1. induction on 3. intros. case H3.
  %% identity
  apply adj_same_result_diff to H2 H7. case H8.
    %% Cut formula principal
    case H1. case H9. case H11.
      apply adj_same_result to H2 H7. case H15. case H12.
       case H10.
       apply merge_move_12 to _ H4 H6.
       apply merge_nil_perm to H21. backchain mll_perm.
        case H20.
      case H14.
    %% Cut formula is not principal -- impossible
    case H9. case H1. case H11.

  %% tensor
  apply adj_same_result_diff to H2 H7. case H13.
    %% cut formula is the tensor -- rank decreases
    case H1. apply par_inv to H5 H4.
      apply adj_1_is_list to H18. apply adj_1_is_list to H11. apply merge_exists to *H21 *H20.
      apply IH to H16 H11 H12 H18 H19 H22.
      apply merge_unadj_2 to H22 H17.
      apply adj_1_is_list to H24. apply adj_1_is_list to H9. apply merge_exists to *H27 *H26.
      apply IH to H15 H9 H10 H24 H23 H28.
      apply perm_sym to *H14. apply perm_merge_3 to *H8 *H30.
      apply merge_assoc to *H31 *H25 *H28 *H6. backchain mll_perm with K = L1.
   %% cut formula is some other formula -- height decreases
   apply merge_unadj_3 to H8 H14. case H15.
     %% cut formula goes to left operand
     apply adj_swap to H16 H9.
     apply add_to_merge_left to H18 H17. rename M to UKK1.
     ass : assert 0 exists UKK, merge U KK UKK.
       apply adj_1_is_list to H19. apply adj_1_is_list to H4.
       apply merge_exists to H22 H23. search.
       case ass.
     Hi : apply IH1 to H1 H19 H10 H4 H5 H22.
     apply merge_unadj_1 to H22 H18.
     ass : assert 0 exists V, merge LL2 KK1 V.
       apply adj_1_is_list to H23. apply adj_1_is_list to H11. apply merge_exists to H25 H26.
       search. case ass.
     ass : assert 0 exists VT, adj V (tens A1 B1) VT.
       apply merge_3_is_list to H25. apply adj_2_is_o to H7. apply adj_exists to H27 H26.
       search. case ass.
     assert mll VT.
     apply adj_swap to H14 H7. apply adj_same_result to H2 *H29.
     apply perm_merge_1 to *H6 *H30.
     apply merge_unadj_1 to H31 H28.
     assert 0 perm VT LL.
       unfold. witness tens A1 B1. witness V. witness LL3. split. search. search.
       assert merge KK1 JJ2 KK2. backchain merge_sym.
       assert merge KK1 LL2 V. backchain merge_sym.
       backchain merge_assoc with J = KK1, K = JJ2, L = KK, JK = KK2, KL = LL2.
     backchain mll_perm with K = VT.

     %% cut formula goes to the right operand
     apply adj_swap to H16 H11.
     apply add_to_merge_right to H18 H17. rename M to UJJ1.
     ass : assert 0 exists UKK, merge U KK UKK.
       apply adj_1_is_list to H19. apply adj_1_is_list to H4.
       apply merge_exists to H22 H23. search.
       case ass.
     Hi : apply IH1 to H1 H19 H12 H4 H5 H22.
     apply merge_unadj_1 to H22 H18.
     ass : assert 0 exists V, merge JJ1 LL2 V.
       apply adj_1_is_list to H9. apply adj_1_is_list to H23. apply merge_exists to H25 H26.
       search. case ass.
     ass : assert 0 exists VT, adj V (tens A1 B1) VT.
       apply merge_3_is_list to H25. apply adj_2_is_o to H7. apply adj_exists to H27 H26.
       search. case ass.
     assert mll VT.
     apply adj_swap to H14 H7. apply adj_same_result to H2 *H29.
     apply perm_merge_1 to *H6 *H30.
     apply merge_unadj_1 to H31 H28.
     assert 0 perm VT LL.
       unfold. witness tens A1 B1. witness V. witness LL3. split. search. search.
       backchain merge_assoc with J = JJ1, K = KK3, L = KK, JK = KK2, KL = LL2.
     backchain mll_perm with K = VT.

  %% one
  case H2.
    case H1. apply merge_nil_perm to H6.
    apply bot_inv to H5 H4.
    backchain mll_perm with K = KK.

    case H8.

  %% par
  apply adj_same_result_diff to H2 H7. case H11.
    %% left cut formula cannot be a par because it is positive
    case H1.

    %% cut formula goes up in left premise
    apply adj_swap to H12 *H8.
    apply adj_swap to *H14 *H9.
    ass : assert 0 exists V, merge U1 KK V.
      apply adj_1_is_list to H16. apply adj_1_is_list to H4. apply merge_exists to H17 H18.
      search. case ass.
    Hi : apply IH1 to H1 H16 H10 H4 H5 H17.
    apply merge_unadj_1 to *H17 *H15.
    apply merge_unadj_1 to *H19 *H13.
    ass : assert 0 exists VV, adj LL3 (par A1 B1) VV.
      apply adj_1_is_list to H20. apply adj_2_is_o to H7. apply adj_exists to H23 H22.
      search. case ass.
    assert mll VV.
    assert 0 perm VV LL.
      apply adj_swap to *H12 *H7.
      apply adj_same_result to *H2 *H25.
      apply perm_merge_1 to *H6 *H26.
      apply merge_unadj_1 to H27 H24.
      unfold. witness par A1 B1. witness LL3. witness LL4. split. search. search.
      backchain merge_perm_det.
    backchain mll_perm with K = VV.

  %% bot
  apply adj_same_result_diff to H2 H7. case H9.
    %% left cut formula cannot be bot because it is positive.
    case H1.

    %% cut formula goes up in left premise
    ass : assert 0 exists V, merge KK1 KK V.
      apply adj_1_is_list to H10. apply adj_1_is_list to H4. apply merge_exists to H11 H12.
      search. case ass.
    Hi : apply IH1 to H1 H10 H8 H4 H5 H11.
    ass : assert 0 exists VV, adj V bot VV.
      apply merge_3_is_list to H11. apply adj_exists to _ H12 with A = bot.
      search. case ass.
    assert mll VV.
    assert 0 perm VV LL.
      apply adj_swap to *H10 *H7.
      apply adj_same_result to *H2 *H15.
      apply perm_merge_1 to *H6 *H16.
      apply merge_unadj_1 to H17 H14.
      unfold. witness bot. witness V. witness LL2. split. search. search.
      backchain merge_perm_det.
    backchain mll_perm with K = VV.