{"header":{"message":"Split project into modules and files.","description":null,"timestamp":"2022-02-07T18:42:48.717655509Z","authors":[{}]},"hash":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC","authors":[{"login":"finegeometer","key":"64ARLu9ao3fdRKWR644xoCX9eBBEMzfkyWsK7kYdkcxn"}],"deps":{"hashes":[["MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC","Split project into modules and files."],["AA",null],["TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC","A nicer implementation, with a fatal flaw."],["KGR5JUMOE7TS5IYPHLW3JHQAVVLNIQDUTIMRFTWLUS3KKLMYQH5AC","Initialize project, and start README."],["J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC","Implement a basic affine lambda calculus."],["RENCWCXSW7BSK53SX6GTVRB2GVCZK5X737S72MNJF6RJGDIRH52AC",""]],"deps":["TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC"],"known":["KGR5JUMOE7TS5IYPHLW3JHQAVVLNIQDUTIMRFTWLUS3KKLMYQH5AC","J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC"]},"hunks":[{"FileAdd":{"meta":{"basename":"uses.v","metadata":0},"context":[{"change":3,"pos":20}],"contents":[{"Add":{"text":"From iris.base_logic Require Import lib.iprop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:78"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:79"}},{"Add":{"text":"Module Type uses_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:102"}},{"Add":{"text":" Parameter uses : Set.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:128"}},{"Add":{"text":" Parameter prop : ∀ {Σ}, uses -> iProp Σ -> iProp Σ.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:189"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:190"}},{"Add":{"text":" Parameter one : uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:216"}},{"Add":{"text":" Axiom one_spec : ∀ {Σ} {P : iProp Σ}, prop one P ⊣⊢ P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:283"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:284"}},{"Add":{"text":" Parameter sep : uses -> uses -> uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:326"}},{"Add":{"text":" Axiom sep_spec : ∀ {Σ} {P : iProp Σ} u v, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:377"}},{"Add":{"text":" prop (sep u v) P ⊢ prop u P ∗ prop v P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:429"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:430"}},{"Add":{"text":" Parameter and : uses -> uses -> uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:472"}},{"Add":{"text":" Axiom and_spec : ∀ {Σ} {P : iProp Σ} u v, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:523"}},{"Add":{"text":" prop (and u v) P ⊢ prop u P ∧ prop v P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:575"}},{"Add":{"text":"End uses_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:590"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:591"}},{"Add":{"text":"Module uses <: uses_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:617"}},{"Add":{"text":" Inductive usesT := One | Many.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:652"}},{"Add":{"text":" Definition uses := usesT.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:682"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:683"}},{"Add":{"text":" Definition prop {Σ} (u : uses) (P : iProp Σ) : iProp Σ := match u with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:761"}},{"Add":{"text":" | One => P","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:780"}},{"Add":{"text":" | Many => □P","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:803"}},{"Add":{"text":" end.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:812"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:813"}},{"Add":{"text":" Definition one := One.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:840"}},{"Add":{"text":" Theorem one_spec {Σ} {P : iProp Σ} : prop one P ⊣⊢ P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:904"}},{"Add":{"text":" Proof. done. Qed. ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:930"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:931"}},{"Add":{"text":" Definition sep (u : uses) (v : uses) : uses := Many.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:988"}},{"Add":{"text":" Theorem sep_spec {Σ} {P : iProp Σ} u v","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1033"}},{"Add":{"text":" : prop (sep u v) P ⊢ prop u P ∗ prop v P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1087"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1098"}},{"Add":{"text":" have: ∀ x, □P ⊢ prop x P by case; [apply: bi.intuitionistically_elim | ].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1186"}},{"Add":{"text":" move=> lemma.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1208"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1209"}},{"Add":{"text":" simpl.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1224"}},{"Add":{"text":" rewrite bi.intuitionistically_sep_dup.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1271"}},{"Add":{"text":" apply: bi.sep_mono; apply: lemma.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1313"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1322"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1323"}},{"Add":{"text":" Definition and (u : uses) (v : uses) : uses := match u, v with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1390"}},{"Add":{"text":" | One, One => One","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1416"}},{"Add":{"text":" | _, _ => Many","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1439"}},{"Add":{"text":" end.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1448"}},{"Add":{"text":" Theorem and_spec {Σ} {P : iProp Σ} u v","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1493"}},{"Add":{"text":" : prop (and u v) P ⊢ prop u P ∧ prop v P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1547"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1558"}},{"Add":{"text":" apply: bi.and_intro; case u; case v; try done; apply: bi.intuitionistically_elim.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1648"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1657"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1658"}},{"Add":{"text":"End uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1668"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":1,"ins":{"up_context":[{"change":3,"pos":53}],"down_context":[{"change":3,"pos":53}],"flag":"BLOCK","start":1670,"end":1705,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":53},"to":{"change":3,"start":0,"end":53},"introduced_by":3}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"From stdpp Require Import strings.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1704"}}],"del_contents":[{"Del":{"text":"From stdpp Require Import binders strings stringmap.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:52"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":3,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":100},"to":{"change":2,"start":0,"end":30},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":30},"to":{"change":3,"start":124,"end":587},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":124},"to":{"change":3,"start":124,"end":587},"introduced_by":3}],"inode":{"change":3,"pos":53}}},"contents":[{"Del":{"text":"(* Set Implicit Arguments. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:29"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:124"}},{"Del":{"text":"(* Nicer error messages. Instead of being asked to prove `False`,","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:190"}},{"Del":{"text":" you are asked to prove `error (hopefully useful message)`.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:253"}},{"Del":{"text":"*)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:256"}},{"Del":{"text":"Module Type errorT.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:276"}},{"Del":{"text":" Parameter error : ∀ {T : Type}, T -> Prop.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:325"}},{"Del":{"text":" Axiom error_elim : ∀ {msgType} {msg : msgType} {T}, error msg -> T.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:399"}},{"Del":{"text":"End errorT.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:411"}},{"Del":{"text":"Module Export error : errorT.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:441"}},{"Del":{"text":" Definition error {T} (msg : T) := False.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:486"}},{"Del":{"text":" Theorem error_elim {msgType} (msg : msgType) T : error msg -> T. Proof. elim. Qed.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:573"}},{"Del":{"text":"End error.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:584"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:585"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:586"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":4,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":588}],"down_context":[{"change":3,"pos":588}],"flag":"BLOCK","start":1706,"end":1733,"inode":{"change":3,"pos":53}}},"contents":[{"Add":{"text":"Require uses context expr.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1732"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":6,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":589}],"down_context":[{"change":3,"pos":743}],"flag":"BLOCK","start":1734,"end":1822,"inode":{"change":3,"pos":53}}},"contents":[{"Add":{"text":"Module context := context.context uses.uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1778"}},{"Add":{"text":"Module Export expr := (expr.expr context).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1821"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":9,"ins":{"up_context":[{"change":3,"pos":744}],"down_context":[],"flag":"BLOCK","start":1823,"end":1841,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":744},"to":{"change":2,"start":31,"end":117},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":117},"to":{"change":3,"start":1295,"end":1296},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1295},"to":{"change":3,"start":1295,"end":1296},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1296},"to":{"change":2,"start":118,"end":231},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":231},"to":{"change":3,"start":1517,"end":1523},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1517},"to":{"change":3,"start":1517,"end":1523},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1523},"to":{"change":2,"start":232,"end":404},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":404},"to":{"change":3,"start":1632,"end":1639},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1632},"to":{"change":3,"start":1632,"end":1639},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1639},"to":{"change":2,"start":405,"end":605},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":605},"to":{"change":3,"start":1736,"end":1742},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1736},"to":{"change":3,"start":1736,"end":1742},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1742},"to":{"change":2,"start":606,"end":834},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":834},"to":{"change":3,"start":1851,"end":1858},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1851},"to":{"change":3,"start":1851,"end":1858},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1858},"to":{"change":2,"start":835,"end":921},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":921},"to":{"change":3,"start":1956,"end":1963},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1956},"to":{"change":3,"start":1956,"end":1963},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1987},"to":{"change":3,"start":1987,"end":1988},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2150},"to":{"change":3,"start":2150,"end":2151},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2191},"to":{"change":3,"start":2191,"end":2194},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2194},"to":{"change":2,"start":922,"end":1268},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":1268},"to":{"change":3,"start":2358,"end":2359},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2358},"to":{"change":3,"start":2358,"end":2359},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2359},"to":{"change":2,"start":1269,"end":1403},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":1403},"to":{"change":3,"start":2359,"end":2360},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2359},"to":{"change":3,"start":2359,"end":2360},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2360},"to":{"change":2,"start":1404,"end":2583},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":2583},"to":{"change":3,"start":2403,"end":2404},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2403},"to":{"change":3,"start":2403,"end":2404},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2404},"to":{"change":2,"start":2584,"end":4420},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":4420},"to":{"change":3,"start":2434,"end":2435},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2434},"to":{"change":3,"start":2434,"end":2435},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":3578},"to":{"change":3,"start":3578,"end":3579},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":3579},"to":{"change":2,"start":4421,"end":5619},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":5619},"to":{"change":3,"start":4090,"end":4091},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":4090},"to":{"change":3,"start":4090,"end":4091},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":4091},"to":{"change":2,"start":5620,"end":5698},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":5698},"to":{"change":3,"start":4246,"end":4247},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":4246},"to":{"change":3,"start":4246,"end":4247},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":4247},"to":{"change":2,"start":5699,"end":6309},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":6309},"to":{"change":3,"start":6631,"end":6636},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":6631},"to":{"change":3,"start":6631,"end":6636},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":6636},"to":{"change":2,"start":6310,"end":6497},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":6497},"to":{"change":3,"start":6636,"end":6637},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":6636},"to":{"change":3,"start":6636,"end":6637},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":6637},"to":{"change":2,"start":6498,"end":13371},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":13371},"to":{"change":3,"start":7306,"end":7308},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7306},"to":{"change":3,"start":7306,"end":7308},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7308},"to":{"change":2,"start":13372,"end":13865},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":13865},"to":{"change":3,"start":7308,"end":7309},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7308},"to":{"change":3,"start":7308,"end":7309},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7309},"to":{"change":2,"start":13866,"end":13972},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":13972},"to":{"change":3,"start":7403,"end":7410},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7403},"to":{"change":3,"start":7403,"end":7410},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7410},"to":{"change":2,"start":13973,"end":14612},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":14612},"to":{"change":3,"start":7502,"end":7533},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7502},"to":{"change":3,"start":7502,"end":7533},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8171},"to":{"change":3,"start":8171,"end":8177},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8177},"to":{"change":2,"start":14613,"end":14827},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":14827},"to":{"change":3,"start":8263,"end":8270},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8263},"to":{"change":3,"start":8263,"end":8270},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8270},"to":{"change":2,"start":14828,"end":15102},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":15102},"to":{"change":3,"start":8293,"end":8320},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8293},"to":{"change":3,"start":8293,"end":8320},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8320},"to":{"change":2,"start":15103,"end":15162},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":15162},"to":{"change":3,"start":8382,"end":8401},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8382},"to":{"change":3,"start":8382,"end":8401},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8401},"to":{"change":2,"start":15163,"end":15262},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":15262},"to":{"change":3,"start":8479,"end":8485},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8479},"to":{"change":3,"start":8479,"end":8485},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8485},"to":{"change":2,"start":15263,"end":15512},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":15512},"to":{"change":3,"start":8485,"end":8487},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8485},"to":{"change":3,"start":8485,"end":8487},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8487},"to":{"change":2,"start":15513,"end":15514},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Export uses.uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1840"}}],"del_contents":[{"Del":{"text":"(* TODO: Should I put this in a module, with a `:>`? *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:86"}},{"Del":{"text":"Inductive uses := One | Many.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:116"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1295"}},{"Del":{"text":"Definition uses_prop {Σ} (u : uses) (P : iProp Σ) : iProp Σ := match u with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:196"}},{"Del":{"text":" | One => P","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:211"}},{"Del":{"text":" | Many => □P","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:230"}},{"Del":{"text":"end.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1521"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1522"}},{"Del":{"text":"Definition uses_sep (u : uses) (v : uses) : uses := Many.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:289"}},{"Del":{"text":"Lemma uses_sep_spec {Σ} {P : iProp Σ} u v","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:333"}},{"Del":{"text":" : uses_prop (uses_sep u v) P ⊢ uses_prop u P ∗ uses_prop v P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:403"}},{"Del":{"text":"Proof.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1638"}},{"Del":{"text":" have: ∀ x, □P ⊢ uses_prop x P by case; [apply: bi.intuitionistically_elim | ].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:493"}},{"Del":{"text":" move=> lemma.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:511"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:512"}},{"Del":{"text":" simpl.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:523"}},{"Del":{"text":" rewrite bi.intuitionistically_sep_dup.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:566"}},{"Del":{"text":" apply: bi.sep_mono; apply: lemma.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:604"}},{"Del":{"text":"Qed.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1740"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1741"}},{"Del":{"text":"Definition uses_and (u : uses) (v : uses) : uses := match u, v with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:673"}},{"Del":{"text":" | One, One => One","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:695"}},{"Del":{"text":" | _, _ => Many","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:714"}},{"Del":{"text":"end.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:719"}},{"Del":{"text":"Lemma uses_and_spec {Σ} {P : iProp Σ} u v","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:763"}},{"Del":{"text":" : uses_prop (uses_and u v) P ⊢ uses_prop u P ∧ uses_prop v P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:833"}},{"Del":{"text":"Proof.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1857"}},{"Del":{"text":" apply: bi.and_intro; case u; case v; try done; apply: bi.intuitionistically_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:920"}},{"Del":{"text":"Qed.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1960"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1961"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1962"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1987"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2150"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2191"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2192"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2193"}},{"Del":{"text":"Module Type contextT.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:943"}},{"Del":{"text":" (* Describes what must hold for an expression to typecheck.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1007"}},{"Del":{"text":" Includes:","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1025"}},{"Del":{"text":" - Free variables, associated with their types and usage patterns.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1099"}},{"Del":{"text":" - Equality constraints, generated during typechecking.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1162"}},{"Del":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1169"}},{"Del":{"text":" Parameter context : gFunctors -> Type.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1212"}},{"Del":{"text":" Parameter prop : ∀ {Σ}, context Σ -> iProp Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1267"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2358"}},{"Del":{"text":" Parameter var : ∀ {Σ}, string -> iProp Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1332"}},{"Del":{"text":" Axiom var_spec : ∀ {Σ} v (T : iProp Σ), prop (var v T) ⊢ T.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1402"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2359"}},{"Del":{"text":" Parameter constrain : ∀ {Σ}, Prop -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1473"}},{"Del":{"text":" Axiom constrain_spec : ∀ {Σ} P (ctx : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1531"}},{"Del":{"text":" prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1587"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1588"}},{"Del":{"text":" (* Combine two expressions, in a separating way. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1644"}},{"Del":{"text":" Parameter sep : ∀ {Σ}, context Σ -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1714"}},{"Del":{"text":" Axiom sep_spec : ∀ {Σ} (c1 c2 : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1766"}},{"Del":{"text":" prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1816"}},{"Del":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1821"}},{"Del":{"text":" (* Combine two expressions, in a non-separating way. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1881"}},{"Del":{"text":" Parameter and : ∀ {Σ}, context Σ -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1951"}},{"Del":{"text":" Axiom and_spec : ∀ {Σ} (c1 c2 : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2003"}},{"Del":{"text":" prop (and c1 c2) ⊢ prop c1 ∧ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2053"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2054"}},{"Del":{"text":" (* Remove a free variable from the context.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2102"}},{"Del":{"text":" Used to implement variable patterns.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2147"}},{"Del":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2154"}},{"Del":{"text":" Parameter bind : ∀ {Σ}, string -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2221"}},{"Del":{"text":" (* Get the type and usage pattern of a variable. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2277"}},{"Del":{"text":" Parameter lookup : ∀ {Σ}, string -> context Σ -> option (iProp Σ * uses).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2360"}},{"Del":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2365"}},{"Del":{"text":" Axiom bind_spec : ∀ {Σ} var (c : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2418"}},{"Del":{"text":" match lookup var c with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2450"}},{"Del":{"text":" | None => emp","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2476"}},{"Del":{"text":" | Some (P, uses) => (uses_prop uses P)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2527"}},{"Del":{"text":" end ∗ prop (bind var c) ⊢ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2566"}},{"Del":{"text":" prop c.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2582"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2403"}},{"Del":{"text":" (* Interpret the expression in the toplevel scope.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2638"}},{"Del":{"text":" This will return a collection of constraints.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2692"}},{"Del":{"text":" Note that the constraint may be something like","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2747"}},{"Del":{"text":" (error (\"Variables not in scope.\", [\"x\", \"y\"])).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2804"}},{"Del":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2811"}},{"Del":{"text":" Parameter toplevel : ∀ {Σ}, context Σ -> Prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2866"}},{"Del":{"text":" Axiom toplevel_spec : ∀ {Σ} (ctx : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2921"}},{"Del":{"text":" toplevel ctx -> ⊢ prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2959"}},{"Del":{"text":"End contextT.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2973"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2974"}},{"Del":{"text":"Module context <: contextT.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3002"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3003"}},{"Del":{"text":" (* It turns out to be easier to carry the equality constraints ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3071"}},{"Del":{"text":" along with the variables, until they are bound.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3127"}},{"Del":{"text":" Afterward, I store the constraints separately.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3182"}},{"Del":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3189"}},{"Del":{"text":" Record contextT {Σ} : Type := {","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3226"}},{"Del":{"text":" Constraints : Prop;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3254"}},{"Del":{"text":" Variables : stringmap (iProp Σ * uses * Prop);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3310"}},{"Del":{"text":" }.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3317"}},{"Del":{"text":" Definition context Σ : Type := contextT (Σ := Σ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3374"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3375"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3376"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3377"}},{"Del":{"text":" Definition prop {Σ} (ctx : context Σ) : iProp Σ := ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3436"}},{"Del":{"text":" ∃ _ : Constraints ctx,","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3469"}},{"Del":{"text":" [∗ map] data ∈ Variables ctx, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3512"}},{"Del":{"text":" let '(P, u, constraints) := data in ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3561"}},{"Del":{"text":" ∃ _ : (constraints : Prop), uses_prop u P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3618"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3619"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3620"}},{"Del":{"text":" Definition var {Σ} (var : string) (type : iProp Σ) : context Σ := {|","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3696"}},{"Del":{"text":" Constraints := True;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3725"}},{"Del":{"text":" Variables := {[var := (type, One, True)]};","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3776"}},{"Del":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3784"}},{"Del":{"text":" Theorem var_spec {Σ} v (T : iProp Σ) : prop (var v T) ⊢ T.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3851"}},{"Del":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3862"}},{"Del":{"text":" apply: bi.exist_elim; move=> [].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3903"}},{"Del":{"text":" rewrite big_sepM_singleton.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3939"}},{"Del":{"text":" apply: bi.exist_elim; move=> [].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3980"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3994"}},{"Del":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4003"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4004"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4005"}},{"Del":{"text":" Definition constrain {Σ} (constraint : Prop) (ctx : context Σ) : context Σ := {|","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4093"}},{"Del":{"text":" Constraints := constraint ∧ Constraints ctx;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4148"}},{"Del":{"text":" Variables := Variables ctx;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4184"}},{"Del":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4192"}},{"Del":{"text":" Theorem constrain_spec {Σ} P (ctx : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4245"}},{"Del":{"text":" : prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4303"}},{"Del":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4314"}},{"Del":{"text":" apply: bi.exist_elim. move=> [wP w].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4359"}},{"Del":{"text":" do 2 apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4396"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4410"}},{"Del":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4419"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2434"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3578"}},{"Del":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4429"}},{"Del":{"text":" Lemma big_sepM_hetero {type : bi} `{countable : Countable K} {V1 V2} ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4503"}},{"Del":{"text":" (Φ : K -> V1 -> type) (Ψ : K -> V2 -> type)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4557"}},{"Del":{"text":" (m1 : gmap K V1) (m2 : gmap K V2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4599"}},{"Del":{"text":" : (∀ k, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4618"}},{"Del":{"text":" (if m1 !! k is Some v then Φ k v else emp) ⊢ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4679"}},{"Del":{"text":" (if m2 !! k is Some v then Ψ k v else emp))","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4736"}},{"Del":{"text":" -> ([∗ map] k ↦ v ∈ m1, Φ k v) ⊢ ([∗ map] k ↦ v ∈ m2, Ψ k v).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4822"}},{"Del":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4833"}},{"Del":{"text":" move: m2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4851"}},{"Del":{"text":" induction m1 as [|k v1 m1' fact1 IH1] using map_ind.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4912"}},{"Del":{"text":" - move=> m2 H. rewrite big_sepM_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4959"}},{"Del":{"text":" induction m2 as [|k v2 m2' fact2 IH2] using map_ind.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5024"}},{"Del":{"text":" + by rewrite big_sepM_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5065"}},{"Del":{"text":" + rewrite big_sepM_insert; last exact fact2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5122"}},{"Del":{"text":" rewrite -(bi.emp_sep emp%I).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5167"}},{"Del":{"text":" apply: bi.sep_mono.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5203"}},{"Del":{"text":" * move: (H k) => H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5240"}},{"Del":{"text":" by rewrite lookup_empty lookup_insert in H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5305"}},{"Del":{"text":" * apply: IH2 => k'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5341"}},{"Del":{"text":" rewrite lookup_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5383"}},{"Del":{"text":" case: (decide (k = k')).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5428"}},{"Del":{"text":" -- move=><-. by rewrite fact2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5479"}},{"Del":{"text":" -- move=> neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5514"}},{"Del":{"text":" move: (H k').","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5552"}},{"Del":{"text":" by rewrite lookup_empty lookup_insert_ne.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5618"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4090"}},{"Del":{"text":" - move=> m2 H.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5642"}},{"Del":{"text":" rewrite big_sepM_insert; last exact fact1.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5697"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4246"}},{"Del":{"text":" apply: transitivity.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5731"}},{"Del":{"text":" { ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5746"}},{"Del":{"text":" apply: bi.sep_mono.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5782"}},{"Del":{"text":" - move: (H k) => H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5819"}},{"Del":{"text":" rewrite lookup_insert in H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5868"}},{"Del":{"text":" exact: H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5899"}},{"Del":{"text":" - apply: (IH1 (delete k m2)) => k'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5951"}},{"Del":{"text":" case: (decide (k = k')).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5996"}},{"Del":{"text":" + move=><-. by rewrite fact1 lookup_delete.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6060"}},{"Del":{"text":" + move=> neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6094"}},{"Del":{"text":" rewrite lookup_delete_ne; last exact neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6160"}},{"Del":{"text":" move: (H k').","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6198"}},{"Del":{"text":" rewrite lookup_insert_ne; last exact neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6264"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6294"}},{"Del":{"text":" }","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6308"}},{"Del":{"text":" ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6635"}},{"Del":{"text":" have: m2 !! k = m2 !! k by []; case: {-1}(m2 !! k) => [v2|] fact2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6388"}},{"Del":{"text":" + by rewrite (big_sepM_delete _ m2).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6437"}},{"Del":{"text":" + by rewrite bi.emp_sep delete_notin.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6487"}},{"Del":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6496"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6636"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6498"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6499"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6500"}},{"Del":{"text":" Definition sep {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6580"}},{"Del":{"text":" Constraints := Constraints c1 ∧ Constraints c2;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6638"}},{"Del":{"text":" Variables := union_with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6670"}},{"Del":{"text":" (λ '(P, u, c1) '(Q, v, c2), Some (P, uses_sep u v, c1 ∧ c2 ∧ P = Q)) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6757"}},{"Del":{"text":" (Variables c1) (Variables c2);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6800"}},{"Del":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6808"}},{"Del":{"text":" Theorem sep_spec {Σ} (c1 c2 : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6855"}},{"Del":{"text":" : prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6907"}},{"Del":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6918"}},{"Del":{"text":" rewrite /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6941"}},{"Del":{"text":" apply: bi.exist_elim; move => [w1 w2].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6988"}},{"Del":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7044"}},{"Del":{"text":" rewrite bi.sep_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7100"}},{"Del":{"text":" clear w1 w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7121"}},{"Del":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7130"}},{"Del":{"text":" apply: transitivity; last (","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7166"}},{"Del":{"text":" apply: bi.sep_mono;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7198"}},{"Del":{"text":" [ apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7236"}},{"Del":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7262"}},{"Del":{"text":" if Variables c1 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7332"}},{"Del":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7402"}},{"Del":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7437"}},{"Del":{"text":" (Variables (sep c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7483"}},{"Del":{"text":" | apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7521"}},{"Del":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7547"}},{"Del":{"text":" if Variables c2 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7617"}},{"Del":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7687"}},{"Del":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7722"}},{"Del":{"text":" (Variables (sep c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7768"}},{"Del":{"text":" ]","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7782"}},{"Del":{"text":" ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7793"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7794"}},{"Del":{"text":" - rewrite -big_sepM_sep.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7827"}},{"Del":{"text":" apply: big_sepM_mono => k [[P u] constraints] fact.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7891"}},{"Del":{"text":" apply: bi.exist_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7925"}},{"Del":{"text":" move: fact; rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7976"}},{"Del":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8044"}},{"Del":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8112"}},{"Del":{"text":" simpl; last done;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8142"}},{"Del":{"text":" move=>w; injection w; clear w;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8185"}},{"Del":{"text":" move=> <-<-<- w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8214"}},{"Del":{"text":" + move: w => [w1 [w2 <-]].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8253"}},{"Del":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8317"}},{"Del":{"text":" rewrite bi.sep_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8381"}},{"Del":{"text":" apply: uses_sep_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8419"}},{"Del":{"text":" + by rewrite bi.sep_emp; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8480"}},{"Del":{"text":" + by rewrite bi.emp_sep; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8541"}},{"Del":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8578"}},{"Del":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8646"}},{"Del":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8714"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8732"}},{"Del":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8769"}},{"Del":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8837"}},{"Del":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8905"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8923"}},{"Del":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8932"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8933"}},{"Del":{"text":" Definition and {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9013"}},{"Del":{"text":" Constraints := Constraints c1 ∧ Constraints c2;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9071"}},{"Del":{"text":" Variables := union_with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9103"}},{"Del":{"text":" (λ '(P, u, c1) '(Q, v, c2), Some (P, uses_and u v, c1 ∧ c2 ∧ P = Q)) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9190"}},{"Del":{"text":" (Variables c1) (Variables c2);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9233"}},{"Del":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9241"}},{"Del":{"text":" Theorem and_spec {Σ} (c1 c2 : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9288"}},{"Del":{"text":" : prop (and c1 c2) ⊢ prop c1 ∧ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9340"}},{"Del":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9351"}},{"Del":{"text":" rewrite /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9374"}},{"Del":{"text":" apply: bi.exist_elim; move => [w1 w2].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9421"}},{"Del":{"text":" rewrite bi.and_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9477"}},{"Del":{"text":" rewrite bi.and_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9533"}},{"Del":{"text":" clear w1 w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9554"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9555"}},{"Del":{"text":" apply: transitivity; last (","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9591"}},{"Del":{"text":" apply: bi.and_mono;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9623"}},{"Del":{"text":" [ apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9661"}},{"Del":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9687"}},{"Del":{"text":" if Variables c1 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9757"}},{"Del":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9827"}},{"Del":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9862"}},{"Del":{"text":" (Variables (and c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9908"}},{"Del":{"text":" | apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9946"}},{"Del":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9972"}},{"Del":{"text":" if Variables c2 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10042"}},{"Del":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10112"}},{"Del":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10147"}},{"Del":{"text":" (Variables (and c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10193"}},{"Del":{"text":" ]","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10207"}},{"Del":{"text":" ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10218"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10219"}},{"Del":{"text":" - rewrite -big_sepM_and. ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10253"}},{"Del":{"text":" apply: big_sepM_mono => k [[P u] constraints] fact.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10317"}},{"Del":{"text":" apply: bi.exist_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10351"}},{"Del":{"text":" move: fact; rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10402"}},{"Del":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10470"}},{"Del":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10538"}},{"Del":{"text":" simpl; last done;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10568"}},{"Del":{"text":" move=>w; injection w; clear w;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10611"}},{"Del":{"text":" move=> <-<-<- w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10640"}},{"Del":{"text":" + move: w => [w1 [w2 <-]].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10679"}},{"Del":{"text":" rewrite bi.and_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10743"}},{"Del":{"text":" rewrite bi.and_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10807"}},{"Del":{"text":" apply: uses_and_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10845"}},{"Del":{"text":" + by rewrite bi.and_True; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10907"}},{"Del":{"text":" + by rewrite bi.True_and; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10969"}},{"Del":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11006"}},{"Del":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11074"}},{"Del":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11142"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11160"}},{"Del":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11197"}},{"Del":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11265"}},{"Del":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11333"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11351"}},{"Del":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11360"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11361"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11362"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11363"}},{"Del":{"text":" Definition bind {Σ} (var : string) (ctx : context Σ) : context Σ := {|","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11441"}},{"Del":{"text":" Variables := delete var (Variables ctx);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11490"}},{"Del":{"text":" Constraints := Constraints ctx ∧ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11534"}},{"Del":{"text":" if Variables ctx !! var is Some (_, _, constraints)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11598"}},{"Del":{"text":" then constraints ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11628"}},{"Del":{"text":" else True;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11651"}},{"Del":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11659"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11660"}},{"Del":{"text":" Definition lookup {Σ} (var : string) (ctx : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11721"}},{"Del":{"text":" : option (iProp Σ * uses)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11756"}},{"Del":{"text":" := option_map fst (Variables ctx !! var).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11802"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11803"}},{"Del":{"text":" Theorem bind_spec {Σ} var (c : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11851"}},{"Del":{"text":" : match lookup var c with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11885"}},{"Del":{"text":" | None => emp","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11911"}},{"Del":{"text":" | Some (P, uses) => (uses_prop uses P)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11962"}},{"Del":{"text":" end ∗ prop (bind var c) ⊢ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12001"}},{"Del":{"text":" prop c.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12017"}},{"Del":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12028"}},{"Del":{"text":" rewrite /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12051"}},{"Del":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12105"}},{"Del":{"text":" move=> [w1 w2].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12129"}},{"Del":{"text":" apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12161"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12162"}},{"Del":{"text":" rewrite /lookup.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12187"}},{"Del":{"text":" move: w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12205"}},{"Del":{"text":" have: Variables c !! var = Variables c !! var by [];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12266"}},{"Del":{"text":" case: {-1}(Variables c !! var) => [[[P u] constraints]|] fact w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12344"}},{"Del":{"text":" - simpl.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12361"}},{"Del":{"text":" rewrite (big_sepM_delete _ (Variables c)); last exact fact.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12433"}},{"Del":{"text":" rewrite bi.sep_exist_r. apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12493"}},{"Del":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12511"}},{"Del":{"text":" - simpl. ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12529"}},{"Del":{"text":" by rewrite bi.emp_sep delete_notin.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12577"}},{"Del":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12586"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12587"}},{"Del":{"text":" Definition toplevel {Σ} (ctx : context Σ) : Prop :=","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12645"}},{"Del":{"text":" if decide (Variables ctx = ∅) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12686"}},{"Del":{"text":" then Constraints ctx","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12715"}},{"Del":{"text":" else error (","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12736"}},{"Del":{"text":" \"Variables not in scope.\", ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12776"}},{"Del":{"text":" map fst (map_to_list (Variables ctx))","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12826"}},{"Del":{"text":" ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12837"}},{"Del":{"text":" Theorem toplevel_spec {Σ} (ctx : context Σ) :","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12889"}},{"Del":{"text":" toplevel ctx -> ⊢ prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12927"}},{"Del":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12938"}},{"Del":{"text":" rewrite /toplevel /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12971"}},{"Del":{"text":" case: (decide (Variables ctx = ∅)) => [-> | _] w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13031"}},{"Del":{"text":" - apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13065"}},{"Del":{"text":" by rewrite big_sepM_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13104"}},{"Del":{"text":" - by apply: error_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13136"}},{"Del":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13145"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13146"}},{"Del":{"text":"End context.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13159"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13160"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13161"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13162"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13163"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13164"}},{"Del":{"text":"Inductive expr {Σ : gFunctors} : iProp Σ -> Type :=","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13218"}},{"Del":{"text":" | Var {T} : string -> expr T","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13251"}},{"Del":{"text":" | Lam {T1 T2} : string -> expr T2 -> expr (T1 -∗ T2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13310"}},{"Del":{"text":" | Pair {T1 T2} : expr T1 -> expr T2 -> expr (T1 ∗ T2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13370"}},{"Del":{"text":".","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7307"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13372"}},{"Del":{"text":"Fixpoint check_expr {Σ} {type : iProp Σ} (e : expr type) : context.context Σ := match e with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13468"}},{"Del":{"text":" | Var var => context.var var type","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13506"}},{"Del":{"text":" | @Lam _ T1 T2 var e =>","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13534"}},{"Del":{"text":" let ctx := check_expr e in","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13569"}},{"Del":{"text":" context.constrain","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13595"}},{"Del":{"text":" (match context.lookup var ctx with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13642"}},{"Del":{"text":" | Some (T, uses) => T = T1 ∧ uses = One","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13700"}},{"Del":{"text":" | None => True","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13731"}},{"Del":{"text":" end)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13748"}},{"Del":{"text":" (context.bind var (check_expr e))","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13794"}},{"Del":{"text":" | Pair e1 e2 => context.sep (check_expr e1) (check_expr e2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13858"}},{"Del":{"text":"end.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13863"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13864"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7308"}},{"Del":{"text":"Lemma check_expr_spec {Σ} (type : iProp Σ) (e : expr type) : ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13929"}},{"Del":{"text":" context.prop (check_expr e) ⊢ type.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13971"}},{"Del":{"text":"Proof.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7409"}},{"Del":{"text":" elim e; simpl.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13991"}},{"Del":{"text":" - move=> T var. apply: context.var_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14036"}},{"Del":{"text":" - move=> T1 T2 var body H.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14067"}},{"Del":{"text":" apply: transitivity; first apply: context.constrain_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14133"}},{"Del":{"text":" apply: bi.exist_elim => w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14168"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14169"}},{"Del":{"text":" apply: bi.wand_intro_r.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14201"}},{"Del":{"text":" apply: transitivity; last apply: H.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14245"}},{"Del":{"text":" apply: transitivity; last apply: (context.bind_spec var).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14311"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14312"}},{"Del":{"text":" rewrite {1}bi.sep_comm.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14344"}},{"Del":{"text":" apply: bi.sep_mono_l.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14374"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14375"}},{"Del":{"text":" move: w; case: (context.lookup var (check_expr body)) => [[P u]|].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14450"}},{"Del":{"text":" + by move=>[->->].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14477"}},{"Del":{"text":" + move=>[]. apply: bi.True_intro.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14519"}},{"Del":{"text":" - move=> T1 T2 e1 H1 e2 H2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14551"}},{"Del":{"text":" apply: transitivity; first apply: context.sep_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14611"}},{"Del":{"text":" by apply: bi.sep_mono.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7532"}},{"Del":{"text":"Qed.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8175"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8176"}},{"Del":{"text":"Definition check_program {Σ} {type : iProp Σ} (e : expr type) : Prop :=","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14686"}},{"Del":{"text":" context.toplevel (check_expr e).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14723"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14724"}},{"Del":{"text":"Theorem check_program_spec {Σ} {type : iProp Σ} (e : expr type) : ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14793"}},{"Del":{"text":" check_program e -> ⊢ type.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14826"}},{"Del":{"text":"Proof.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8269"}},{"Del":{"text":" move=> w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14841"}},{"Del":{"text":" apply: transitivity.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14866"}},{"Del":{"text":" - apply: context.toplevel_spec w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14904"}},{"Del":{"text":" - apply: check_expr_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14934"}},{"Del":{"text":"Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14939"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14940"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14941"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14942"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14943"}},{"Del":{"text":"(* Example Proof. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14964"}},{"Del":{"text":"Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15010"}},{"Del":{"text":" move=> Σ P Q.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15029"}},{"Del":{"text":" apply: (check_program_spec (Lam \"x\" (Var \"x\"))).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15082"}},{"Del":{"text":" by vm_compute.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15101"}},{"Del":{"text":"Qed.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8297"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8298"}},{"Del":{"text":"(* Example Proof. *)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8319"}},{"Del":{"text":"Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15161"}},{"Del":{"text":" move=> Σ P Q.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8400"}},{"Del":{"text":" apply: (check_program_spec (Lam \"x\" (Lam \"y\" (Pair (Var \"y\") (Var \"x\"))))).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15242"}},{"Del":{"text":" by vm_compute.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15261"}},{"Del":{"text":"Qed.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8483"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8484"}},{"Del":{"text":"(* Example Proof. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15283"}},{"Del":{"text":"Goal ∀ {Σ} (P Q R : iProp Σ), ⊢ P -∗ Q -∗ R -∗ (R ∗ Q) ∗ P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15359"}},{"Del":{"text":" move=> Σ P Q R.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15380"}},{"Del":{"text":" apply: (check_program_spec (Lam \"x\" (Lam \"y\" (Lam \"z\" (Pair (Pair (Var \"z\") (Var \"y\")) (Var \"x\")))))).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15487"}},{"Del":{"text":" by vm_compute.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15506"}},{"Del":{"text":"Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15511"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8485"}},{"Del":{"text":"","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8486"}},{"Del":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15513"}}]}},{"FileAdd":{"meta":{"basename":"expr.v","metadata":0},"context":[{"change":3,"pos":20}],"contents":[{"Add":{"text":"From stdpp Require Import strings.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1908"}},{"Add":{"text":"From iris.base_logic Require Import lib.iprop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1955"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1956"}},{"Add":{"text":"Require uses context.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1978"}},{"Add":{"text":"Import uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1991"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:1992"}},{"Add":{"text":"Module Type expr_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2015"}},{"Add":{"text":" Parameter expr : ∀ {Σ}, iProp Σ -> Type.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2064"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2065"}},{"Add":{"text":" Parameter check_program : ∀ {Σ} {type : iProp Σ}, expr type -> Prop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2142"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2143"}},{"Add":{"text":" Axiom check_program_spec : ∀ {Σ} {type : iProp Σ} (e : expr type),","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2218"}},{"Add":{"text":" check_program e -> ⊢ type.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2255"}},{"Add":{"text":"End expr_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2270"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2271"}},{"Add":{"text":"Module expr (context : context.context_spec uses).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2322"}},{"Add":{"text":" Inductive exprT {Σ : gFunctors} : iProp Σ -> Type :=","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2381"}},{"Add":{"text":" | Var {T} : string -> exprT T","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2419"}},{"Add":{"text":" | Lam {T1 T2} : string -> exprT T2 -> exprT (T1 -∗ T2)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2484"}},{"Add":{"text":" | Pair {T1 T2} : exprT T1 -> exprT T2 -> exprT (T1 ∗ T2)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2551"}},{"Add":{"text":" .","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2557"}},{"Add":{"text":" Definition expr {Σ} := exprT (Σ := Σ).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2603"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2604"}},{"Add":{"text":" Fixpoint check_expr {Σ} {type : iProp Σ} (e : expr type) : context.context Σ := match e with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2704"}},{"Add":{"text":" | Var var => context.var var type","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2746"}},{"Add":{"text":" | @Lam _ T1 T2 var e =>","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2778"}},{"Add":{"text":" let ctx := check_expr e in","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2817"}},{"Add":{"text":" context.constrain","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2847"}},{"Add":{"text":" (match context.lookup var ctx with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2898"}},{"Add":{"text":" | Some (T, uses) => T = T1 ∧ uses = uses.One","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:2965"}},{"Add":{"text":" | None => True","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3000"}},{"Add":{"text":" end)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3021"}},{"Add":{"text":" (context.bind var (check_expr e))","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3071"}},{"Add":{"text":" | Pair e1 e2 => context.sep (check_expr e1) (check_expr e2)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3139"}},{"Add":{"text":" end.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3148"}},{"Add":{"text":" ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3153"}},{"Add":{"text":" Lemma check_expr_spec {Σ} (type : iProp Σ) (e : expr type) : ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3221"}},{"Add":{"text":" context.prop (check_expr e) ⊢ type.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3267"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3278"}},{"Add":{"text":" elim e; simpl.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3301"}},{"Add":{"text":" - move=> T var. apply: context.var_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3350"}},{"Add":{"text":" - move=> T1 T2 var body H.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3385"}},{"Add":{"text":" apply: transitivity; first apply: context.constrain_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3455"}},{"Add":{"text":" apply: bi.exist_elim => w.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3494"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3495"}},{"Add":{"text":" apply: bi.wand_intro_r.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3531"}},{"Add":{"text":" apply: transitivity; last apply: H.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3579"}},{"Add":{"text":" apply: transitivity; last apply: (context.bind_spec var).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3649"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3650"}},{"Add":{"text":" rewrite {1}bi.sep_comm.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3686"}},{"Add":{"text":" apply: bi.sep_mono_l.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3720"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3721"}},{"Add":{"text":" move: w; case: (context.lookup var (check_expr body)) => [[P u]|].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3800"}},{"Add":{"text":" + by move=>[->->].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3831"}},{"Add":{"text":" + move=>[]. apply: bi.True_intro.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3877"}},{"Add":{"text":" - move=> T1 T2 e1 H1 e2 H2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3913"}},{"Add":{"text":" apply: transitivity; first apply: context.sep_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:3977"}},{"Add":{"text":" by apply: bi.sep_mono.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4012"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4021"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4022"}},{"Add":{"text":" Definition check_program {Σ} {type : iProp Σ} (e : expr type) : Prop :=","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4100"}},{"Add":{"text":" context.toplevel (check_expr e).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4141"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4142"}},{"Add":{"text":" Theorem check_program_spec {Σ} {type : iProp Σ} (e : expr type) : ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4215"}},{"Add":{"text":" check_program e -> ⊢ type.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4252"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4263"}},{"Add":{"text":" move=> w.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4281"}},{"Add":{"text":" apply: transitivity.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4310"}},{"Add":{"text":" - apply: context.toplevel_spec w.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4352"}},{"Add":{"text":" - apply: check_expr_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4386"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4395"}},{"Add":{"text":"End expr.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4405"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4406"}}]}},{"FileAdd":{"meta":{"basename":"error.v","metadata":0},"context":[{"change":3,"pos":20}],"contents":[{"Add":{"text":"(* Nicer error messages. Instead of being asked to prove `False`,","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4506"}},{"Add":{"text":" you are asked to prove `error (hopefully useful message)`.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4569"}},{"Add":{"text":"*)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4572"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4573"}},{"Add":{"text":"Module Type error_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4597"}},{"Add":{"text":" Parameter error : forall {T : Type}, T -> Prop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4649"}},{"Add":{"text":" Axiom error_elim : forall {msgType} {msg : msgType} {T}, error msg -> T.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4726"}},{"Add":{"text":"End error_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4742"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4743"}},{"Add":{"text":"Module Export error : error_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4777"}},{"Add":{"text":" Definition error {T} (msg : T) := False.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4822"}},{"Add":{"text":" Definition error_elim {msgType} (msg : msgType) T : error msg -> T := False_rect T.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4910"}},{"Add":{"text":"End error.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:4921"}}]}},{"FileAdd":{"meta":{"basename":"context.v","metadata":0},"context":[{"change":3,"pos":20}],"contents":[{"Add":{"text":"From stdpp Require Import binders strings stringmap.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5010"}},{"Add":{"text":"From iris.base_logic Require Import lib.iprop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5057"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5058"}},{"Add":{"text":"Require Import error uses.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5085"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5086"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5087"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5088"}},{"Add":{"text":"Module Type context_spec (uses : uses_spec).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5133"}},{"Add":{"text":" (* Describes what must hold for an expression to typecheck.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5197"}},{"Add":{"text":" Includes:","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5215"}},{"Add":{"text":" - Free variables, associated with their types and usage patterns.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5289"}},{"Add":{"text":" - Equality constraints, generated during typechecking.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5352"}},{"Add":{"text":" *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5359"}},{"Add":{"text":" Parameter context : gFunctors -> Type.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5402"}},{"Add":{"text":" Parameter prop : ∀ {Σ}, context Σ -> iProp Σ.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5457"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5458"}},{"Add":{"text":" Parameter var : ∀ {Σ}, string -> iProp Σ -> context Σ.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5522"}},{"Add":{"text":" Axiom var_spec : ∀ {Σ} v (T : iProp Σ), prop (var v T) ⊢ T.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5592"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5593"}},{"Add":{"text":" Parameter constrain : ∀ {Σ}, Prop -> context Σ -> context Σ.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5663"}},{"Add":{"text":" Axiom constrain_spec : ∀ {Σ} P (ctx : context Σ),","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5721"}},{"Add":{"text":" prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5777"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5778"}},{"Add":{"text":" (* Combine two expressions, in a separating way. *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5834"}},{"Add":{"text":" Parameter sep : ∀ {Σ}, context Σ -> context Σ -> context Σ.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5904"}},{"Add":{"text":" Axiom sep_spec : ∀ {Σ} (c1 c2 : context Σ),","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:5956"}},{"Add":{"text":" prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6006"}},{"Add":{"text":" ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6011"}},{"Add":{"text":" (* Combine two expressions, in a non-separating way. *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6071"}},{"Add":{"text":" Parameter and : ∀ {Σ}, context Σ -> context Σ -> context Σ.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6141"}},{"Add":{"text":" Axiom and_spec : ∀ {Σ} (c1 c2 : context Σ),","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6193"}},{"Add":{"text":" prop (and c1 c2) ⊢ prop c1 ∧ prop c2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6243"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6244"}},{"Add":{"text":" (* Remove a free variable from the context.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6292"}},{"Add":{"text":" Used to implement variable patterns.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6337"}},{"Add":{"text":" *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6344"}},{"Add":{"text":" Parameter bind : ∀ {Σ}, string -> context Σ -> context Σ.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6411"}},{"Add":{"text":" (* Get the type and usage pattern of a variable. *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6467"}},{"Add":{"text":" Parameter lookup : ∀ {Σ}, string -> context Σ -> option (iProp Σ * uses.uses).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6555"}},{"Add":{"text":" ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6560"}},{"Add":{"text":" Axiom bind_spec : ∀ {Σ} var (c : context Σ),","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6613"}},{"Add":{"text":" match lookup var c with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6645"}},{"Add":{"text":" | None => emp","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6671"}},{"Add":{"text":" | Some (P, uses) => (uses.prop uses P)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6722"}},{"Add":{"text":" end ∗ prop (bind var c) ⊢ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6761"}},{"Add":{"text":" prop c.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6777"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6778"}},{"Add":{"text":" (* Interpret the expression in the toplevel scope.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6833"}},{"Add":{"text":" This will return a collection of constraints.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6887"}},{"Add":{"text":" Note that the constraint may be something like","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6942"}},{"Add":{"text":" (error (\"Variables not in scope.\", [\"x\", \"y\"])).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:6999"}},{"Add":{"text":" *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7006"}},{"Add":{"text":" Parameter toplevel : ∀ {Σ}, context Σ -> Prop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7061"}},{"Add":{"text":" Axiom toplevel_spec : ∀ {Σ} (ctx : context Σ),","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7116"}},{"Add":{"text":" toplevel ctx -> ⊢ prop ctx.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7154"}},{"Add":{"text":"End context_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7172"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7173"}},{"Add":{"text":"Module context (uses : uses_spec) <: context_spec(uses).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7230"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7231"}},{"Add":{"text":" (* It turns out to be easier to carry the equality constraints ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7299"}},{"Add":{"text":" along with the variables, until they are bound.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7355"}},{"Add":{"text":" Afterward, I store the constraints separately.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7410"}},{"Add":{"text":" *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7417"}},{"Add":{"text":" Record contextT {Σ} : Type := {","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7454"}},{"Add":{"text":" Constraints : Prop;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7482"}},{"Add":{"text":" Variables : stringmap (iProp Σ * uses.uses * Prop);","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7543"}},{"Add":{"text":" }.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7550"}},{"Add":{"text":" Definition context Σ : Type := contextT (Σ := Σ).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7607"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7608"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7609"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7610"}},{"Add":{"text":" Definition prop {Σ} (ctx : context Σ) : iProp Σ := ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7669"}},{"Add":{"text":" ∃ _ : Constraints ctx,","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7702"}},{"Add":{"text":" [∗ map] data ∈ Variables ctx, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7745"}},{"Add":{"text":" let '(P, u, constraints) := data in ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7794"}},{"Add":{"text":" ∃ _ : (constraints : Prop), uses.prop u P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7851"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7852"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7853"}},{"Add":{"text":" Definition var {Σ} (var : string) (type : iProp Σ) : context Σ := {|","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7929"}},{"Add":{"text":" Constraints := True;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:7958"}},{"Add":{"text":" Variables := {[var := (type, uses.one, True)]};","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8014"}},{"Add":{"text":" |}.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8022"}},{"Add":{"text":" Theorem var_spec {Σ} v (T : iProp Σ) : prop (var v T) ⊢ T.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8089"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8100"}},{"Add":{"text":" apply: bi.exist_elim; move=> [].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8141"}},{"Add":{"text":" rewrite big_sepM_singleton.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8177"}},{"Add":{"text":" apply: bi.exist_elim; move=> [].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8218"}},{"Add":{"text":" by rewrite uses.one_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8252"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8261"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8262"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8263"}},{"Add":{"text":" Definition constrain {Σ} (constraint : Prop) (ctx : context Σ) : context Σ := {|","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8351"}},{"Add":{"text":" Constraints := constraint ∧ Constraints ctx;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8406"}},{"Add":{"text":" Variables := Variables ctx;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8442"}},{"Add":{"text":" |}.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8450"}},{"Add":{"text":" Theorem constrain_spec {Σ} P (ctx : context Σ)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8503"}},{"Add":{"text":" : prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8561"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8572"}},{"Add":{"text":" apply: bi.exist_elim. move=> [wP w].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8617"}},{"Add":{"text":" do 2 apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8654"}},{"Add":{"text":" done.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8668"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8677"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8678"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8679"}},{"Add":{"text":" ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8688"}},{"Add":{"text":" Lemma big_sepM_hetero {type : bi} `{countable : Countable K} {V1 V2} ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8762"}},{"Add":{"text":" (Φ : K -> V1 -> type) (Ψ : K -> V2 -> type)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8816"}},{"Add":{"text":" (m1 : gmap K V1) (m2 : gmap K V2)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8858"}},{"Add":{"text":" : (∀ k, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8877"}},{"Add":{"text":" (if m1 !! k is Some v then Φ k v else emp) ⊢ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8938"}},{"Add":{"text":" (if m2 !! k is Some v then Ψ k v else emp))","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:8995"}},{"Add":{"text":" -> ([∗ map] k ↦ v ∈ m1, Φ k v) ⊢ ([∗ map] k ↦ v ∈ m2, Ψ k v).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9081"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9092"}},{"Add":{"text":" move: m2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9110"}},{"Add":{"text":" induction m1 as [|k v1 m1' fact1 IH1] using map_ind.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9171"}},{"Add":{"text":" - move=> m2 H. rewrite big_sepM_empty.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9218"}},{"Add":{"text":" induction m2 as [|k v2 m2' fact2 IH2] using map_ind.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9283"}},{"Add":{"text":" + by rewrite big_sepM_empty.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9324"}},{"Add":{"text":" + rewrite big_sepM_insert; last exact fact2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9381"}},{"Add":{"text":" rewrite -(bi.emp_sep emp%I).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9426"}},{"Add":{"text":" apply: bi.sep_mono.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9462"}},{"Add":{"text":" * move: (H k) => H'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9499"}},{"Add":{"text":" by rewrite lookup_empty lookup_insert in H'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9564"}},{"Add":{"text":" * apply: IH2 => k'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9600"}},{"Add":{"text":" rewrite lookup_empty.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9642"}},{"Add":{"text":" case: (decide (k = k')).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9687"}},{"Add":{"text":" -- move=><-. by rewrite fact2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9738"}},{"Add":{"text":" -- move=> neq.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9773"}},{"Add":{"text":" move: (H k').","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9811"}},{"Add":{"text":" by rewrite lookup_empty lookup_insert_ne.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9877"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9878"}},{"Add":{"text":" - move=> m2 H.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9901"}},{"Add":{"text":" rewrite big_sepM_insert; last exact fact1.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9956"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9957"}},{"Add":{"text":" apply: transitivity.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:9990"}},{"Add":{"text":" { ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10005"}},{"Add":{"text":" apply: bi.sep_mono.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10041"}},{"Add":{"text":" - move: (H k) => H'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10078"}},{"Add":{"text":" rewrite lookup_insert in H'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10127"}},{"Add":{"text":" exact: H'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10158"}},{"Add":{"text":" - apply: (IH1 (delete k m2)) => k'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10210"}},{"Add":{"text":" case: (decide (k = k')).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10255"}},{"Add":{"text":" + move=><-. by rewrite fact1 lookup_delete.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10319"}},{"Add":{"text":" + move=> neq.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10353"}},{"Add":{"text":" rewrite lookup_delete_ne; last exact neq.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10419"}},{"Add":{"text":" move: (H k').","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10457"}},{"Add":{"text":" rewrite lookup_insert_ne; last exact neq.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10523"}},{"Add":{"text":" done.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10553"}},{"Add":{"text":" }","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10567"}},{"Add":{"text":" ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10572"}},{"Add":{"text":" have: m2 !! k = m2 !! k by []; case: {-1}(m2 !! k) => [v2|] fact2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10651"}},{"Add":{"text":" + by rewrite (big_sepM_delete _ m2).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10700"}},{"Add":{"text":" + by rewrite bi.emp_sep delete_notin.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10750"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10759"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10760"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10761"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10762"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10763"}},{"Add":{"text":" Definition sep {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10843"}},{"Add":{"text":" Constraints := Constraints c1 ∧ Constraints c2;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10901"}},{"Add":{"text":" Variables := union_with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:10933"}},{"Add":{"text":" (λ '(P, u, c1) '(Q, v, c2), Some (P, uses.sep u v, c1 ∧ c2 ∧ P = Q)) ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11020"}},{"Add":{"text":" (Variables c1) (Variables c2);","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11063"}},{"Add":{"text":" |}.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11071"}},{"Add":{"text":" Theorem sep_spec {Σ} (c1 c2 : context Σ)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11118"}},{"Add":{"text":" : prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11170"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11181"}},{"Add":{"text":" rewrite /prop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11204"}},{"Add":{"text":" apply: bi.exist_elim; move => [w1 w2].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11251"}},{"Add":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11307"}},{"Add":{"text":" rewrite bi.sep_exist_r; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11363"}},{"Add":{"text":" clear w1 w2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11384"}},{"Add":{"text":" ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11393"}},{"Add":{"text":" apply: transitivity; last (","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11429"}},{"Add":{"text":" apply: bi.sep_mono;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11461"}},{"Add":{"text":" [ apply: (big_sepM_hetero","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11499"}},{"Add":{"text":" (λ k _, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11525"}},{"Add":{"text":" if Variables c1 !! k is Some (P, u, constraints) ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11595"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses.prop u P ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11665"}},{"Add":{"text":" else emp)%I _ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11700"}},{"Add":{"text":" (Variables (sep c1 c2))) => k","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11746"}},{"Add":{"text":" | apply: (big_sepM_hetero","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11784"}},{"Add":{"text":" (λ k _, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11810"}},{"Add":{"text":" if Variables c2 !! k is Some (P, u, constraints) ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11880"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses.prop u P ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11950"}},{"Add":{"text":" else emp)%I _ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:11985"}},{"Add":{"text":" (Variables (sep c1 c2))) => k","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12031"}},{"Add":{"text":" ]","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12045"}},{"Add":{"text":" ).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12056"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12057"}},{"Add":{"text":" - rewrite -big_sepM_sep.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12090"}},{"Add":{"text":" apply: big_sepM_mono => k [[P u] constraints] fact.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12154"}},{"Add":{"text":" apply: bi.exist_elim.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12188"}},{"Add":{"text":" move: fact; rewrite lookup_union_with.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12239"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12307"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12375"}},{"Add":{"text":" simpl; last done;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12405"}},{"Add":{"text":" move=>w; injection w; clear w;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12448"}},{"Add":{"text":" move=> <-<-<- w.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12477"}},{"Add":{"text":" + move: w => [w1 [w2 <-]].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12516"}},{"Add":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12580"}},{"Add":{"text":" rewrite bi.sep_exist_r; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12644"}},{"Add":{"text":" apply: uses.sep_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12682"}},{"Add":{"text":" + by rewrite bi.sep_emp; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12743"}},{"Add":{"text":" + by rewrite bi.emp_sep; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12804"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12841"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12909"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12977"}},{"Add":{"text":" done.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:12995"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13032"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13100"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13168"}},{"Add":{"text":" done.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13186"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13195"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13196"}},{"Add":{"text":" Definition and {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13276"}},{"Add":{"text":" Constraints := Constraints c1 ∧ Constraints c2;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13334"}},{"Add":{"text":" Variables := union_with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13366"}},{"Add":{"text":" (λ '(P, u, c1) '(Q, v, c2), Some (P, uses.and u v, c1 ∧ c2 ∧ P = Q)) ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13453"}},{"Add":{"text":" (Variables c1) (Variables c2);","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13496"}},{"Add":{"text":" |}.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13504"}},{"Add":{"text":" Theorem and_spec {Σ} (c1 c2 : context Σ)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13551"}},{"Add":{"text":" : prop (and c1 c2) ⊢ prop c1 ∧ prop c2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13603"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13614"}},{"Add":{"text":" rewrite /prop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13637"}},{"Add":{"text":" apply: bi.exist_elim; move => [w1 w2].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13684"}},{"Add":{"text":" rewrite bi.and_exist_l; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13740"}},{"Add":{"text":" rewrite bi.and_exist_r; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13796"}},{"Add":{"text":" clear w1 w2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13817"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13818"}},{"Add":{"text":" apply: transitivity; last (","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13854"}},{"Add":{"text":" apply: bi.and_mono;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13886"}},{"Add":{"text":" [ apply: (big_sepM_hetero","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13924"}},{"Add":{"text":" (λ k _, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:13950"}},{"Add":{"text":" if Variables c1 !! k is Some (P, u, constraints) ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14020"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses.prop u P ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14090"}},{"Add":{"text":" else emp)%I _ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14125"}},{"Add":{"text":" (Variables (and c1 c2))) => k","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14171"}},{"Add":{"text":" | apply: (big_sepM_hetero","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14209"}},{"Add":{"text":" (λ k _, ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14235"}},{"Add":{"text":" if Variables c2 !! k is Some (P, u, constraints) ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14305"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses.prop u P ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14375"}},{"Add":{"text":" else emp)%I _ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14410"}},{"Add":{"text":" (Variables (and c1 c2))) => k","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14456"}},{"Add":{"text":" ]","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14470"}},{"Add":{"text":" ).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14481"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14482"}},{"Add":{"text":" - rewrite -big_sepM_and. ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14516"}},{"Add":{"text":" apply: big_sepM_mono => k [[P u] constraints] fact.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14580"}},{"Add":{"text":" apply: bi.exist_elim.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14614"}},{"Add":{"text":" move: fact; rewrite lookup_union_with.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14665"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14733"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14801"}},{"Add":{"text":" simpl; last done;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14831"}},{"Add":{"text":" move=>w; injection w; clear w;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14874"}},{"Add":{"text":" move=> <-<-<- w.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14903"}},{"Add":{"text":" + move: w => [w1 [w2 <-]].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:14942"}},{"Add":{"text":" rewrite bi.and_exist_l; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15006"}},{"Add":{"text":" rewrite bi.and_exist_r; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15070"}},{"Add":{"text":" apply: uses.and_spec.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15108"}},{"Add":{"text":" + by rewrite bi.and_True; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15170"}},{"Add":{"text":" + by rewrite bi.True_and; apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15232"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15269"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15337"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15405"}},{"Add":{"text":" done.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15423"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15460"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15528"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15596"}},{"Add":{"text":" done.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15614"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15623"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15624"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15625"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15626"}},{"Add":{"text":" Definition bind {Σ} (var : string) (ctx : context Σ) : context Σ := {|","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15704"}},{"Add":{"text":" Variables := delete var (Variables ctx);","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15753"}},{"Add":{"text":" Constraints := Constraints ctx ∧ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15797"}},{"Add":{"text":" if Variables ctx !! var is Some (_, _, constraints)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15861"}},{"Add":{"text":" then constraints ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15891"}},{"Add":{"text":" else True;","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15914"}},{"Add":{"text":" |}.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15922"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15923"}},{"Add":{"text":" Definition lookup {Σ} (var : string) (ctx : context Σ)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:15984"}},{"Add":{"text":" : option (iProp Σ * uses.uses)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16024"}},{"Add":{"text":" := option_map fst (Variables ctx !! var).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16070"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16071"}},{"Add":{"text":" Theorem bind_spec {Σ} var (c : context Σ)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16119"}},{"Add":{"text":" : match lookup var c with","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16153"}},{"Add":{"text":" | None => emp","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16179"}},{"Add":{"text":" | Some (P, uses) => (uses.prop uses P)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16230"}},{"Add":{"text":" end ∗ prop (bind var c) ⊢ ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16269"}},{"Add":{"text":" prop c.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16285"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16296"}},{"Add":{"text":" rewrite /prop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16319"}},{"Add":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_elim.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16373"}},{"Add":{"text":" move=> [w1 w2].","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16397"}},{"Add":{"text":" apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16429"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16430"}},{"Add":{"text":" rewrite /lookup.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16455"}},{"Add":{"text":" move: w2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16473"}},{"Add":{"text":" have: Variables c !! var = Variables c !! var by [];","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16534"}},{"Add":{"text":" case: {-1}(Variables c !! var) => [[[P u] constraints]|] fact w2.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16612"}},{"Add":{"text":" - simpl.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16629"}},{"Add":{"text":" rewrite (big_sepM_delete _ (Variables c)); last exact fact.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16701"}},{"Add":{"text":" rewrite bi.sep_exist_r. apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16761"}},{"Add":{"text":" done.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16779"}},{"Add":{"text":" - simpl. ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16797"}},{"Add":{"text":" by rewrite bi.emp_sep delete_notin.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16845"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16854"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16855"}},{"Add":{"text":" Definition toplevel {Σ} (ctx : context Σ) : Prop :=","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16913"}},{"Add":{"text":" if decide (Variables ctx = ∅) ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16954"}},{"Add":{"text":" then Constraints ctx","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:16983"}},{"Add":{"text":" else error (","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17004"}},{"Add":{"text":" \"Variables not in scope.\", ","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17044"}},{"Add":{"text":" map fst (map_to_list (Variables ctx))","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17094"}},{"Add":{"text":" ).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17105"}},{"Add":{"text":" Theorem toplevel_spec {Σ} (ctx : context Σ) :","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17157"}},{"Add":{"text":" toplevel ctx -> ⊢ prop ctx.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17195"}},{"Add":{"text":" Proof.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17206"}},{"Add":{"text":" rewrite /toplevel /prop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17239"}},{"Add":{"text":" case: (decide (Variables ctx = ∅)) => [-> | _] w.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17299"}},{"Add":{"text":" - apply: bi.exist_intro'.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17333"}},{"Add":{"text":" by rewrite big_sepM_empty.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17372"}},{"Add":{"text":" - by apply: error_elim.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17404"}},{"Add":{"text":" Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17413"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17414"}},{"Add":{"text":"End context.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17427"}}]}},{"FileAdd":{"meta":{"basename":"examples","metadata":576},"context":[{"change":6,"pos":1}],"contents":[]}},{"FileAdd":{"meta":{"basename":"basic.v","metadata":0},"context":[{"change":0,"pos":17448}],"contents":[{"Add":{"text":"From stdpp Require Import binders strings stringmap.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17535"}},{"Add":{"text":"From iris.base_logic Require Import lib.iprop.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17582"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17583"}},{"Add":{"text":"Require Import lang.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17604"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17605"}},{"Add":{"text":"(* Example Proof. *)","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17626"}},{"Add":{"text":"Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ P.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17672"}},{"Add":{"text":" move=> Σ P Q.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17691"}},{"Add":{"text":" apply: (check_program_spec (Lam \"x\" (Var \"x\"))).","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17744"}},{"Add":{"text":" by vm_compute.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17763"}},{"Add":{"text":"Qed.","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17768"}},{"Add":{"text":"","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17769"}}]}},{"Edit":{"inode":{"change":3,"pos":91},"path":"_CoqProject","line":1,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":91}],"down_context":[{"change":3,"pos":92}],"flag":"BLOCK","start":17771,"end":17839,"inode":{"change":3,"pos":91}}},"contents":[{"Add":{"text":"theories/error.v","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17787"}},{"Add":{"text":"theories/uses.v","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17803"}},{"Add":{"text":"theories/context.v","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17822"}},{"Add":{"text":"theories/expr.v","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17838"}}]}},{"Edit":{"inode":{"change":3,"pos":91},"path":"_CoqProject","line":6,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":108}],"down_context":[{"change":3,"pos":108}],"flag":"BLOCK","start":17840,"end":17857,"inode":{"change":3,"pos":91}}},"contents":[{"Add":{"text":"examples/basic.v","pos":"MEAGJHFJR3UPM3NOKKPWF2L3YQZ2VQS5RK34ZRTLGD24ZBMFRH6AC:17856"}}]}}],"owner":"finegeometer","repo":"iris-curry-howard","token":"ncEI3DygyMwCTu3jlIFqeW13bNU3t55j30S7DZLYhF0=","login":null}

…

Dependencies

Change contents

Review