AUGER_LinearLogic

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.

{{{#!coq (** 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).

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.

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. }}}