AUGER_LinearLogic

Pierre Letouzey edited this page Oct 26, 2017 · 7 revisions

The content of a file for linear logic.

The use of a sequent "m, 1"

∗
…
⊢ …

is not natural and convenient at all for real proving; it is here only to illustrate how to use the Notation system, and what we can do with it.

(** Linear Logic in Coq *)
Require Import Utf8_core.
Require Import List.
Set Implicit Arguments.
Inductive linear_expression: Prop :=
| D: ∀ (is_positive: bool)
       (absolute_value: expression)
, linear_expression
with expression: Prop :=
| A: ∀ (atom: Prop)
, expression
| B: ∀ (left_expression: linear_expression)
       (is_multiplicative: bool)
       (right_expression: linear_expression)
, expression
| C: ∀ (is_multiplicative: bool)
, expression
| E: ∀ (delayed_expression: linear_expression)
, expression
.
Notation "a ⊗ b" := (D true (B a true b)) (at level 30).
Notation "a & b" := (D false (B a false b)) (at level 40).
Notation "a ⊕ b" := (D true (B a false b)) (at level 50).
Notation "a ⅋ b" := (D false (B a true b)) (at level 60).
Notation "𝟘" := (D true (C false)).
Notation "𝟙" := (D true (C true)).
Notation "⊥" := (D false (C true)).
Notation "⊤" := (D false (C false)).
Notation "! a" := (D true (E a)) (at level 20).
Notation "? a" := (D false (E a)) (at level 20).
Notation "a ⁺" := (D true (A a)) (at level 10, format "a ⁺").
Notation "a ⁻" := (D false (A a)) (at level 10, format "a ⁻").
Example formula (A: Prop) := (?⊥⊕A⁻)⊗!(𝟙&𝟘⅋⊤).
Eval compute in (formula (0>1)).
Fixpoint linear_dual (e: linear_expression) :=
 match e with
 | D pos abs => D (if pos then false else true) (dual abs)
 end
 with dual e :=
 match e with
 | B l m r => B (linear_dual l) m (linear_dual r)
 | E l => E (linear_dual l)
 | _ => e
 end.
Notation "a ⁽⁻⁾" := (linear_dual a) (at level 10).
Eval compute in (λ (P: Prop), (formula P)⁽⁻⁾).
Theorem linear_dual_idempotent: ∀ φ, φ = φ⁽⁻⁾⁽⁻⁾
with dual_idempotent: ∀ ψ, ψ = dual (dual ψ).
  Proof.
  intros [positivity absolute]; simpl.
  case dual_idempotent; case positivity; split.
 Proof.
 intros []; simpl; intros; repeat case linear_dual_idempotent; split.
Qed.
Fixpoint split i (lst: list linear_expression) :=
 match i with
 | O => (nil, lst)
 |S i=> match lst with
        |  nil  => (nil, nil)
        |le::lst=> let (l, r) := split i lst in (le::l, r)
        end
 end.
Inductive all_delayed: list linear_expression → Prop :=
| NoMoreDelays: all_delayed nil
| MoreDelays: ∀ l, all_delayed l → ∀ le, all_delayed (? le::l).
Inductive three_choices: Set := Birth | Life | Death.
Definition why_choice t le :=
 match t with
 | Birth => nil
 | Life => le::nil
 | Death => ? le::? le::nil
 end.
Inductive provable: list linear_expression → Prop :=
| Move: ∀ n l, provable (let (l, r) := split n l in r++l) → provable l
| Atom: ∀ P, provable (P⁺::P⁻::nil)
| Times: ∀ n lst a b, provable (a::(fst (split n lst))) →
                      provable (b::(snd (split n lst))) →
                      provable (a⊗b::lst)
| With: ∀ l a b, provable (a::l) → provable (b::l) → provable (a&b::l)
| Plus: ∀ l a b (c: bool),
        provable ((if c then a else b)::l) → provable (a⊕b::l)
| Par: ∀ l a b, provable (a::b::l) → provable (a⅋b::l)
| One: provable (𝟙::nil)
| Bottom: ∀ l, provable l → provable (⊥::l)
| Top: ∀ l, provable (⊤::l)
| Bang: ∀ l, all_delayed l → ∀ le, provable (le::l) → provable (! le::l)
| Wnot: ∀ l t le, provable ((why_choice t le)++l) → provable (? le::l)
| Cut: ∀ t n lst, provable (t::(fst (split n lst))) →
                  provable (linear_dual t::(snd (split n lst))) →
                  provable lst.
Definition stack tl := List.map linear_dual tl.
Inductive these_provable hd tl : Prop :=
ProvableWrapper: provable (hd::(stack tl)) →
                 these_provable hd tl.
Notation "∗ H1 .. H2 ⊢ J" :=
 (these_provable J (H1::..(H2::nil)..))
 (at level 100, format
  "'[v' ∗ '/' H1 '/' .. '/' H2 '/' ']' ⊢ J"
 ).
Notation "∗ ⊢ J" :=
 (these_provable J nil)
 (at level 100, format
  "'[v' ∗ '/' ']' ⊢ J"
 ).
Tactic Notation "linear" tactic(tac) :=
apply ProvableWrapper;
simpl;
tac;
simpl;
match goal with
| |- provable (?hd::?tl) =>
  cut (these_provable hd (stack tl)); simpl;
  [now intros []; simpl; clear;
   repeat case linear_dual_idempotent
  |repeat case linear_dual_idempotent]
end.
Ltac move_ n :=
apply Move with n.
Ltac times_ n :=
apply Times with n.
Ltac left_ :=
apply Plus with true.
Ltac right_ :=
apply Plus with false.
Ltac bang_ :=
apply Bang; [simpl; repeat constructor|].
Ltac weak_ :=
apply Wnot with Birth.
Ltac derel_ :=
apply Wnot with Life.
Ltac contr_ :=
apply Wnot with Death.
Ltac cut_ t n :=
apply Cut with t n.
Lemma linear_em: ∀ φ, ∗φ⊢φ
with lem: ∀ ψ b, ∗D b ψ ⊢ D b ψ.
  Proof.
  clear -lem; intros [b ψ].
  apply lem.
 Proof.
 clear lem; intros [a|φ₁ μ φ₂|[]|φ];
 ((assert (Φ₁ := linear_em φ₁); assert (Φ₂ := linear_em φ₂))
||(assert (Φ := linear_em φ))
||idtac); (try case μ); intros []; simpl; clear linear_em.
            now linear constructor.
           linear move_ 1.
           now linear constructor.
          linear move_ 1.
          linear constructor; move_ 2.
          now linear times_ 1.
         linear constructor; move_ 2.
         now linear times_ 1; move_ 1.
        linear move_ 1.
        linear constructor; move_ 1.
         now linear left_.
        now linear right_.
       linear constructor; move_ 1.
        now linear left_; move_ 1.
       now linear right_; move_ 1.
      linear move_ 1.
      now linear repeat constructor.
     now linear repeat constructor.
    linear move_ 1.
    now linear constructor.
   now linear constructor.
  linear bang_; move_ 1.
  now linear derel_; move_ 1.
 linear move_ 1.
 linear bang_; move_ 1.
 now linear derel_.
Qed.
Goal ∀ φ, ∗ ⊢φ⁽⁻⁾⅋φ.
 intro φ.
 linear constructor.
 apply linear_em.
Qed.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.