### Implement a basic affine lambda calculus.

Created by  finegeometer  on February 4, 2022
`J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC`
main
##### Change contents
• ###### Insertion in theories/lang.v at line 1 [2.53]
[2.53]
``From stdpp Require Import binders strings stringmap.``From iris.base_logic Require Import lib.iprop.``Set Implicit Arguments.``(* Nicer error messages. Instead of being asked to prove `False`,``    you are asked to prove `error (hopefully useful message)`.``*)``Module Type errorT.``    Parameter error : ∀ {T : Type}, T -> Prop.``    Axiom error_elim : ∀ {msgType} {msg : msgType} {T}, error msg -> T.``End errorT.``Module Export error : errorT.``    Definition error {T} (msg : T) := False.``    Theorem error_elim {msgType} (msg : msgType) T : error msg -> T. Proof. elim. Qed.``End error.``Inductive context Σ : Type :=``    | CEmpty``    | CVar of string & iProp Σ``    | CAnd of context Σ & context Σ``    | CSep of context Σ & context Σ``.``Definition c_sep {Σ} (c1 c2 : context Σ) := ``    if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CSep c1 c2.``Definition c_and {Σ} (c1 c2 : context Σ) := ``    if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CAnd c1 c2.``    ``Fixpoint bind {Σ} (var : string) (c : context Σ) : context Σ ``:= match c with``    | CEmpty _ => CEmpty _``    | CVar var' P => if decide (var = var') then CEmpty _ else CVar var' P``    | CAnd c1 c2 => c_and (bind var c1) (bind var c2)``    | CSep c1 c2 => c_sep (bind var c1) (bind var c2)``end.``Fixpoint prop_of_ctx {Σ} (c : context Σ) : iProp Σ := match c with``    | CEmpty _ => True``    | CVar _ P => P``    | CAnd c1 c2 => prop_of_ctx c1 ∧ prop_of_ctx c2``    | CSep c1 c2 => prop_of_ctx c1 ∗ prop_of_ctx c2``end.``Lemma c_sep_spec {Σ} (c1 c2 : context Σ) ``    : prop_of_ctx (c_sep c1 c2) ⊣⊢ prop_of_ctx (CSep c1 c2).``Proof.``    by case c1; case c2; intros; simpl; ``        try rewrite bi.emp_sep; try rewrite bi.sep_emp.``Qed.``Lemma c_and_spec {Σ} (c1 c2 : context Σ) ``    : prop_of_ctx (c_and c1 c2) ⊣⊢ prop_of_ctx (CAnd c1 c2).``Proof.``    by case c1; case c2; intros; simpl;``        try rewrite bi.True_and; try rewrite bi.and_True.``Qed.``(* Purpose of ctx_uses:``    - Only used in constraint generation``    - Generates equality constraints, if variable is repeated``    - Decides whether the variable needs to be persistent.``    - No, it is also used in bind_spec.``    - MUST determine whether variable needs to be persistent.``    - MUST allow generation of equality constraints.``    - SHOULD allow easy definition of bind_spec.``    option (constraints * iProp * uses)``*)``Inductive uses := One | Many.``(* Returns:``    - Whether the variable must be persistent.``    - The type of the variable.``    - The generated equality constraints.``*)``Fixpoint ctx_uses {Σ} (var : string) (c : context Σ)``    : option (uses * iProp Σ * Prop)``    := match c with``        | CEmpty _ => None``        | CVar var' P =>``            if decide (var = var') ``            then Some (One, P, True)``            else None``        | CAnd c1 c2 =>``            union_with``                (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some``                    ( match u1, u2 with One, One => One | _, _ => Many end``                    , P1``                    , constraints1 ∧ constraints2 ∧ P1 = P2``                    )``                )``                (ctx_uses var c1)``                (ctx_uses var c2)``        | CSep c1 c2 =>``            union_with``                (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some``                    ( Many``                    , P1``                    , constraints1 ∧ constraints2 ∧ P1 = P2``                    )``                )``                (ctx_uses var c1)``                (ctx_uses var c2)``    end.``Lemma bind_spec {Σ} var (c : context Σ)``    : match ctx_uses var c with``        | None => prop_of_ctx (bind var c) ⊢ prop_of_ctx c``        | Some (uses, P, constraints) => ``            constraints -> ``            prop_of_ctx (bind var c) ∗ ``            (match uses with One => P | Many => □P end) ⊢ ``            prop_of_ctx c``    end.``Proof.``    have: ∀ u (P : iProp Σ), □ P ⊢ match u with One => P | Many => □ P end.``    { case. apply: bi.intuitionistically_elim. done. }``    move=> lemma1.``    have: ∀ u (P : iProp Σ), match u with One => P | Many => □ P end ⊢ P.``    { case. done. apply: bi.intuitionistically_elim. }``    move=> lemma2.``    elim c; simpl.``    - done.``    - move=> var' P.``        case: (decide (var = var')).``        + by rewrite bi.emp_sep.``        + done.``    - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;``        move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;``        simpl; rewrite c_and_spec; simpl;``        [ move=>[/H1 w1 [/H2 w2 eq]] ``        | move: H2 => w2 /H1 w1 ``        | move: H1 => w1 /H2 w2 ``        | move: H1 H2 => w1 w2``        ];``        (apply: transitivity; last (apply: bi.and_mono; [apply: w1 | apply: w2])).``        + rewrite eq.``            apply: transitivity; first apply: bi.sep_and_r.``            apply: bi.and_mono; apply: bi.sep_mono_r.``            * case u1; last done.``                apply: transitivity; last apply: (lemma2 u2).``                by case u2.``            * case u2; last by case u1.``                apply: transitivity; last apply: (lemma2 u1).``                by case u1.``            + apply: transitivity; first apply: bi.sep_and_r.``            apply: bi.and_mono; first done.``            rewrite -{2}[prop_of_ctx _]bi.sep_emp.``            apply: bi.sep_mono; first done.``            apply: bi.True_intro.``        + apply: transitivity; first apply: bi.sep_and_r.``            apply: bi.and_mono; last done.``            rewrite -{2}[prop_of_ctx _]bi.sep_emp.``            apply: bi.sep_mono; first done.``            apply: bi.True_intro.``        + done.``    - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;``        move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;``        simpl; rewrite c_sep_spec; simpl;``        [ move=>[/H1 w1 [/H2 w2 eq]] ``        | move: H2 => w2 /H1 w1 ``        | move: H1 => w1 /H2 w2 ``        | move: H1 H2 => w1 w2``        ];``        (apply: transitivity; last (apply: bi.sep_mono; [apply: w1 | apply: w2])).``        + apply: transitivity; ``            last (apply: bi.sep_mono; apply: bi.sep_mono_r; apply: lemma1).``            rewrite eq {1}bi.intuitionistically_sep_dup.``            rewrite bi.sep_assoc bi.sep_assoc; apply: bi.sep_mono_l.``            rewrite -bi.sep_assoc -bi.sep_assoc; apply: bi.sep_mono_r.``            by rewrite bi.sep_comm.``        + by rewrite ``            -bi.sep_assoc ``            [(prop_of_ctx (bind var c2) ∗ _)%I]bi.sep_comm``            bi.sep_assoc.``        + by rewrite bi.sep_assoc.``        + done.``Qed.``    ``Inductive expr {Σ : gFunctors} : context Σ -> iProp Σ -> Type :=``    | Pair {c1 c2 T1 T2} : expr c1 T1 -> expr c2 T2 -> expr (c_sep c1 c2) (T1 ∗ T2)``    | Var {T} : ∀ var, expr (CVar var T) T``    | Lam {ctx T1 T2} ``        : ∀ var {constraints : match ctx_uses var ctx with``            | None => True``            | Some (uses, type, constraints) =>``                constraints ∧ type = T1 ∧ match uses with ``                    | Many => error ``                        ( "A linear variable was used multiple times.", var )``                    | One => True``                end``        end },``        expr ctx T2 ->``        expr (bind var ctx) (T1 -∗ T2)``.``Lemma check_expr {Σ ctx} (type : iProp Σ) : ``    expr ctx type -> prop_of_ctx ctx ⊢ type.``Proof.``    elim.``    - move=> ctx1 ctx2 type1 type2 e1 fact1 e2 fact2.``        rewrite c_sep_spec.``        by apply: bi.sep_mono.``    - done.``    - move=> ctx1 type1 type2 var w e fact1.``        move: (bind_spec var ctx1) w.``        case: (ctx_uses var ctx1) => [[[uses P] constraint]|].``        + case uses; last (move=> _ [_ [_ err]]; apply: (error_elim err)).``            move=> H2 [/H2 fact2 [<- []]].``            apply: bi.wand_intro_r.``            apply: transitivity.``            * apply: fact2.``            * apply: fact1.``        + move=> fact2 [].``            apply: bi.wand_intro_r.``            rewrite -[type2]bi.sep_emp.``            apply: bi.sep_mono.``            * apply: transitivity; [apply: fact2 | apply: fact1].``            * apply: bi.True_intro.``Qed.``Theorem check_program {Σ} (type : iProp Σ) : ``    expr (CEmpty _) type -> ⊢ type.``Proof.``    exact: check_expr.``Qed.``(* Example Proof. *)``Goal forall {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.``    move=> Σ P Q.``    by apply: (check_program (Lam "x" (Lam "y" (Pair (Var "y") (Var "x"))))).``Qed.``
• ###### File addition: TODO.md (----------)
[3.1]
``# My TODO list``## Short term``- Expand the language.``    - Import theorems from outside.``    - Pattern matching.``    - Update monad.``- Add notations.``- Generalize the language to work for an arbitrary BI, rather than specifically iProp.``    - This would require changing it from an *affine* language to a *linear* one.``## Long term``- Explore the idea of combining this with a normal programming language.``    - As in, combine the analysis language with the language it's analyzing.``
• ###### Replacement in README.md at line 9 [2.175]
B:BD[2.622] → [2.622:666]
``This project is an exploration of that idea.``
[2.622]
``This project is an exploration of that idea.``## Versioning``Developed using:``- Coq 8.13.2``- Iris dev.2021-12-17.0.72485828``