{"header":{"message":"A nicer implementation, with a fatal flaw.","description":null,"timestamp":"2022-02-07T01:00:48.474365891Z","authors":[{}]},"hash":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC","authors":[{"login":"finegeometer","key":"64ARLu9ao3fdRKWR644xoCX9eBBEMzfkyWsK7kYdkcxn"}],"deps":{"hashes":[["TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC","A nicer implementation, with a fatal flaw."],["AA",null],["J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC","Implement a basic affine lambda calculus."],["KGR5JUMOE7TS5IYPHLW3JHQAVVLNIQDUTIMRFTWLUS3KKLMYQH5AC","Initialize project, and start README."]],"deps":["J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC"],"known":["KGR5JUMOE7TS5IYPHLW3JHQAVVLNIQDUTIMRFTWLUS3KKLMYQH5AC"]},"hunks":[{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":3,"ins":{"up_context":[{"change":2,"pos":100}],"down_context":[{"change":2,"pos":124}],"flag":"BLOCK","start":0,"end":30,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":100},"to":{"change":2,"start":100,"end":124},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"(* Set Implicit Arguments. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:29"}}],"del_contents":[{"Del":{"text":"Set Implicit Arguments.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:123"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":20,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":589},"to":{"change":2,"start":589,"end":743},"introduced_by":2}],"inode":{"change":3,"pos":53}}},"contents":[{"Del":{"text":"Inductive context Σ : Type :=","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:619"}},{"Del":{"text":" | CEmpty","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:632"}},{"Del":{"text":" | CVar of string & iProp Σ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:664"}},{"Del":{"text":" | CAnd of context Σ & context Σ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:702"}},{"Del":{"text":" | CSep of context Σ & context Σ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:740"}},{"Del":{"text":".","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:742"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":21,"ins":{"up_context":[{"change":2,"pos":744}],"down_context":[{"change":2,"pos":1295}],"flag":"BLOCK","start":31,"end":117,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":744},"to":{"change":2,"start":744,"end":1295},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"(* TODO: Should I put this in a module, with a `:>`? *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:86"}},{"Add":{"text":"Inductive uses := One | Many.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:116"}}],"del_contents":[{"Del":{"text":"Definition c_sep {Σ} (c1 c2 : context Σ) := ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:790"}},{"Del":{"text":" if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CSep c1 c2.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:868"}},{"Del":{"text":"Definition c_and {Σ} (c1 c2 : context Σ) := ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:915"}},{"Del":{"text":" if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CAnd c1 c2.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:993"}},{"Del":{"text":" ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:998"}},{"Del":{"text":"Fixpoint bind {Σ} (var : string) (c : context Σ) : context Σ ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1063"}},{"Del":{"text":":= match c with","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1079"}},{"Del":{"text":" | CEmpty _ => CEmpty _","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1106"}},{"Del":{"text":" | CVar var' P => if decide (var = var') then CEmpty _ else CVar var' P","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1181"}},{"Del":{"text":" | CAnd c1 c2 => c_and (bind var c1) (bind var c2)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1235"}},{"Del":{"text":" | CSep c1 c2 => c_sep (bind var c1) (bind var c2)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1289"}},{"Del":{"text":"end.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1294"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":24,"ins":{"up_context":[{"change":2,"pos":1296}],"down_context":[{"change":2,"pos":1517}],"flag":"BLOCK","start":118,"end":231,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1296},"to":{"change":2,"start":1296,"end":1517},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Definition uses_prop {Σ} (u : uses) (P : iProp Σ) : iProp Σ := match u with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:196"}},{"Add":{"text":" | One => P","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:211"}},{"Add":{"text":" | Many => □P","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:230"}}],"del_contents":[{"Del":{"text":"Fixpoint prop_of_ctx {Σ} (c : context Σ) : iProp Σ := match c with","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1365"}},{"Del":{"text":" | CEmpty _ => True","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1388"}},{"Del":{"text":" | CVar _ P => P","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1408"}},{"Del":{"text":" | CAnd c1 c2 => prop_of_ctx c1 ∧ prop_of_ctx c2","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1462"}},{"Del":{"text":" | CSep c1 c2 => prop_of_ctx c1 ∗ prop_of_ctx c2","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1516"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":29,"ins":{"up_context":[{"change":2,"pos":1523}],"down_context":[{"change":2,"pos":1632}],"flag":"BLOCK","start":232,"end":404,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1523},"to":{"change":2,"start":1523,"end":1632},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Definition uses_sep (u : uses) (v : uses) : uses := Many.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:289"}},{"Add":{"text":"Lemma uses_sep_spec {Σ} {P : iProp Σ} u v","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:333"}},{"Add":{"text":" : uses_prop (uses_sep u v) P ⊢ uses_prop u P ∗ uses_prop v P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:403"}}],"del_contents":[{"Del":{"text":"Lemma c_sep_spec {Σ} (c1 c2 : context Σ) ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1566"}},{"Del":{"text":" : prop_of_ctx (c_sep c1 c2) ⊣⊢ prop_of_ctx (CSep c1 c2).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1631"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":33,"ins":{"up_context":[{"change":2,"pos":1639}],"down_context":[{"change":2,"pos":1736}],"flag":"BLOCK","start":405,"end":605,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1639},"to":{"change":2,"start":1639,"end":1736},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" have: ∀ x, □P ⊢ uses_prop x P by case; [apply: bi.intuitionistically_elim | ].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:493"}},{"Add":{"text":" move=> lemma.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:511"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:512"}},{"Add":{"text":" simpl.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:523"}},{"Add":{"text":" rewrite bi.intuitionistically_sep_dup.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:566"}},{"Add":{"text":" apply: bi.sep_mono; apply: lemma.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:604"}}],"del_contents":[{"Del":{"text":" by case c1; case c2; intros; simpl; ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1679"}},{"Del":{"text":" try rewrite bi.emp_sep; try rewrite bi.sep_emp.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1735"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":41,"ins":{"up_context":[{"change":2,"pos":1742}],"down_context":[{"change":2,"pos":1851}],"flag":"BLOCK","start":606,"end":834,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1742},"to":{"change":2,"start":1742,"end":1851},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Definition uses_and (u : uses) (v : uses) : uses := match u, v with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:673"}},{"Add":{"text":" | One, One => One","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:695"}},{"Add":{"text":" | _, _ => Many","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:714"}},{"Add":{"text":"end.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:719"}},{"Add":{"text":"Lemma uses_and_spec {Σ} {P : iProp Σ} u v","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:763"}},{"Add":{"text":" : uses_prop (uses_and u v) P ⊢ uses_prop u P ∧ uses_prop v P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:833"}}],"del_contents":[{"Del":{"text":"Lemma c_and_spec {Σ} (c1 c2 : context Σ) ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1785"}},{"Del":{"text":" : prop_of_ctx (c_and c1 c2) ⊣⊢ prop_of_ctx (CAnd c1 c2).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1850"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":48,"ins":{"up_context":[{"change":2,"pos":1858}],"down_context":[{"change":2,"pos":1956}],"flag":"BLOCK","start":835,"end":921,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1858},"to":{"change":2,"start":1858,"end":1956},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" apply: bi.and_intro; case u; case v; try done; apply: bi.intuitionistically_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:920"}}],"del_contents":[{"Del":{"text":" by case c1; case c2; intros; simpl;","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1897"}},{"Del":{"text":" try rewrite bi.True_and; try rewrite bi.and_True.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1955"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":52,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1963},"to":{"change":2,"start":1963,"end":1987},"introduced_by":2}],"inode":{"change":3,"pos":53}}},"contents":[{"Del":{"text":"(* Purpose of ctx_uses:","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:1986"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":53,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1988},"to":{"change":2,"start":1988,"end":2150},"introduced_by":2}],"inode":{"change":3,"pos":53}}},"contents":[{"Del":{"text":" - Only used in constraint generation","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2028"}},{"Del":{"text":" - Generates equality constraints, if variable is repeated","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2090"}},{"Del":{"text":" - Decides whether the variable needs to be persistent.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2149"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":54,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2151},"to":{"change":2,"start":2151,"end":2191},"introduced_by":2}],"inode":{"change":3,"pos":53}}},"contents":[{"Del":{"text":" - No, it is also used in bind_spec.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2190"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":57,"ins":{"up_context":[{"change":2,"pos":2194}],"down_context":[{"change":2,"pos":2358}],"flag":"BLOCK","start":922,"end":1268,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2194},"to":{"change":2,"start":2194,"end":2358},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Module Type contextT.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:943"}},{"Add":{"text":" (* Describes what must hold for an expression to typecheck.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1007"}},{"Add":{"text":" Includes:","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1025"}},{"Add":{"text":" - Free variables, associated with their types and usage patterns.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1099"}},{"Add":{"text":" - Equality constraints, generated during typechecking.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1162"}},{"Add":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1169"}},{"Add":{"text":" Parameter context : gFunctors -> Type.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1212"}},{"Add":{"text":" Parameter prop : ∀ {Σ}, context Σ -> iProp Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1267"}}],"del_contents":[{"Del":{"text":" - MUST determine whether variable needs to be persistent.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2255"}},{"Del":{"text":" - MUST allow generation of equality constraints.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2308"}},{"Del":{"text":" - SHOULD allow easy definition of bind_spec.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2357"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":66,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":2359}],"down_context":[{"change":2,"pos":2359}],"flag":"BLOCK","start":1269,"end":1403,"inode":{"change":3,"pos":53}}},"contents":[{"Add":{"text":" Parameter var : ∀ {Σ}, string -> iProp Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1332"}},{"Add":{"text":" Axiom var_spec : ∀ {Σ} v (T : iProp Σ), prop (var v T) ⊢ T.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1402"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":69,"ins":{"up_context":[{"change":2,"pos":2360}],"down_context":[{"change":2,"pos":2403}],"flag":"BLOCK","start":1404,"end":2583,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2360},"to":{"change":2,"start":2360,"end":2403},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" Parameter constrain : ∀ {Σ}, Prop -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1473"}},{"Add":{"text":" Axiom constrain_spec : ∀ {Σ} P (ctx : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1531"}},{"Add":{"text":" prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1587"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1588"}},{"Add":{"text":" (* Combine two expressions, in a separating way. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1644"}},{"Add":{"text":" Parameter sep : ∀ {Σ}, context Σ -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1714"}},{"Add":{"text":" Axiom sep_spec : ∀ {Σ} (c1 c2 : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1766"}},{"Add":{"text":" prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1816"}},{"Add":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1821"}},{"Add":{"text":" (* Combine two expressions, in a non-separating way. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1881"}},{"Add":{"text":" Parameter and : ∀ {Σ}, context Σ -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:1951"}},{"Add":{"text":" Axiom and_spec : ∀ {Σ} (c1 c2 : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2003"}},{"Add":{"text":" prop (and c1 c2) ⊢ prop c1 ∧ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2053"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2054"}},{"Add":{"text":" (* Remove a free variable from the context.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2102"}},{"Add":{"text":" Used to implement variable patterns.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2147"}},{"Add":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2154"}},{"Add":{"text":" Parameter bind : ∀ {Σ}, string -> context Σ -> context Σ.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2221"}},{"Add":{"text":" (* Get the type and usage pattern of a variable. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2277"}},{"Add":{"text":" Parameter lookup : ∀ {Σ}, string -> context Σ -> option (iProp Σ * uses).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2360"}},{"Add":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2365"}},{"Add":{"text":" Axiom bind_spec : ∀ {Σ} var (c : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2418"}},{"Add":{"text":" match lookup var c with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2450"}},{"Add":{"text":" | None => emp","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2476"}},{"Add":{"text":" | Some (P, uses) => (uses_prop uses P)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2527"}},{"Add":{"text":" end ∗ prop (bind var c) ⊢ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2566"}},{"Add":{"text":" prop c.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2582"}}],"del_contents":[{"Del":{"text":" option (constraints * iProp * uses)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2399"}},{"Del":{"text":"*)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2402"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":97,"ins":{"up_context":[{"change":2,"pos":2404}],"down_context":[{"change":2,"pos":2434}],"flag":"BLOCK","start":2584,"end":4420,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2404},"to":{"change":2,"start":2404,"end":2434},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" (* Interpret the expression in the toplevel scope.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2638"}},{"Add":{"text":" This will return a collection of constraints.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2692"}},{"Add":{"text":" Note that the constraint may be something like","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2747"}},{"Add":{"text":" (error (\"Variables not in scope.\", [\"x\", \"y\"])).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2804"}},{"Add":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2811"}},{"Add":{"text":" Parameter toplevel : ∀ {Σ}, context Σ -> Prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2866"}},{"Add":{"text":" Axiom toplevel_spec : ∀ {Σ} (ctx : context Σ),","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2921"}},{"Add":{"text":" toplevel ctx -> ⊢ prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2959"}},{"Add":{"text":"End contextT.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2973"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:2974"}},{"Add":{"text":"Module context <: contextT.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3002"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3003"}},{"Add":{"text":" (* It turns out to be easier to carry the equality constraints ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3071"}},{"Add":{"text":" along with the variables, until they are bound.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3127"}},{"Add":{"text":" Afterward, I store the constraints separately.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3182"}},{"Add":{"text":" *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3189"}},{"Add":{"text":" Record contextT {Σ} : Type := {","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3226"}},{"Add":{"text":" Constraints : Prop;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3254"}},{"Add":{"text":" Variables : stringmap (iProp Σ * uses * Prop);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3310"}},{"Add":{"text":" }.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3317"}},{"Add":{"text":" Definition context Σ : Type := contextT (Σ := Σ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3374"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3375"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3376"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3377"}},{"Add":{"text":" Definition prop {Σ} (ctx : context Σ) : iProp Σ := ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3436"}},{"Add":{"text":" ∃ _ : Constraints ctx,","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3469"}},{"Add":{"text":" [∗ map] data ∈ Variables ctx, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3512"}},{"Add":{"text":" let '(P, u, constraints) := data in ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3561"}},{"Add":{"text":" ∃ _ : (constraints : Prop), uses_prop u P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3618"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3619"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3620"}},{"Add":{"text":" Definition var {Σ} (var : string) (type : iProp Σ) : context Σ := {|","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3696"}},{"Add":{"text":" Constraints := True;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3725"}},{"Add":{"text":" Variables := {[var := (type, One, True)]};","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3776"}},{"Add":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3784"}},{"Add":{"text":" Theorem var_spec {Σ} v (T : iProp Σ) : prop (var v T) ⊢ T.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3851"}},{"Add":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3862"}},{"Add":{"text":" apply: bi.exist_elim; move=> [].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3903"}},{"Add":{"text":" rewrite big_sepM_singleton.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3939"}},{"Add":{"text":" apply: bi.exist_elim; move=> [].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3980"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:3994"}},{"Add":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4003"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4004"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4005"}},{"Add":{"text":" Definition constrain {Σ} (constraint : Prop) (ctx : context Σ) : context Σ := {|","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4093"}},{"Add":{"text":" Constraints := constraint ∧ Constraints ctx;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4148"}},{"Add":{"text":" Variables := Variables ctx;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4184"}},{"Add":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4192"}},{"Add":{"text":" Theorem constrain_spec {Σ} P (ctx : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4245"}},{"Add":{"text":" : prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4303"}},{"Add":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4314"}},{"Add":{"text":" apply: bi.exist_elim. move=> [wP w].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4359"}},{"Add":{"text":" do 2 apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4396"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4410"}},{"Add":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4419"}}],"del_contents":[{"Del":{"text":"Inductive uses := One | Many.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2433"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":153,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2435},"to":{"change":2,"start":2435,"end":3578},"introduced_by":2}],"inode":{"change":3,"pos":53}}},"contents":[{"Del":{"text":"(* Returns:","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2446"}},{"Del":{"text":" - Whether the variable must be persistent.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2493"}},{"Del":{"text":" - The type of the variable.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2525"}},{"Del":{"text":" - The generated equality constraints.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2567"}},{"Del":{"text":"*)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2570"}},{"Del":{"text":"Fixpoint ctx_uses {Σ} (var : string) (c : context Σ)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2625"}},{"Del":{"text":" : option (uses * iProp Σ * Prop)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2663"}},{"Del":{"text":" := match c with","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2683"}},{"Del":{"text":" | CEmpty _ => None","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2710"}},{"Del":{"text":" | CVar var' P =>","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2735"}},{"Del":{"text":" if decide (var = var') ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2771"}},{"Del":{"text":" then Some (One, P, True)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2808"}},{"Del":{"text":" else None","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2830"}},{"Del":{"text":" | CAnd c1 c2 =>","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2854"}},{"Del":{"text":" union_with","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2877"}},{"Del":{"text":" (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:2951"}},{"Del":{"text":" ( match u1, u2 with One, One => One | _, _ => Many end","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3026"}},{"Del":{"text":" , P1","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3051"}},{"Del":{"text":" , constraints1 ∧ constraints2 ∧ P1 = P2","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3115"}},{"Del":{"text":" )","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3137"}},{"Del":{"text":" )","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3155"}},{"Del":{"text":" (ctx_uses var c1)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3189"}},{"Del":{"text":" (ctx_uses var c2)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3223"}},{"Del":{"text":" | CSep c1 c2 =>","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3247"}},{"Del":{"text":" union_with","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3270"}},{"Del":{"text":" (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3344"}},{"Del":{"text":" ( Many","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3371"}},{"Del":{"text":" , P1","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3396"}},{"Del":{"text":" , constraints1 ∧ constraints2 ∧ P1 = P2","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3460"}},{"Del":{"text":" )","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3482"}},{"Del":{"text":" )","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3500"}},{"Del":{"text":" (ctx_uses var c1)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3534"}},{"Del":{"text":" (ctx_uses var c2)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3568"}},{"Del":{"text":" end.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3577"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":154,"ins":{"up_context":[{"change":2,"pos":3579}],"down_context":[{"change":2,"pos":4090}],"flag":"BLOCK","start":4421,"end":5619,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":3579},"to":{"change":2,"start":3579,"end":4090},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4429"}},{"Add":{"text":" Lemma big_sepM_hetero {type : bi} `{countable : Countable K} {V1 V2} ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4503"}},{"Add":{"text":" (Φ : K -> V1 -> type) (Ψ : K -> V2 -> type)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4557"}},{"Add":{"text":" (m1 : gmap K V1) (m2 : gmap K V2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4599"}},{"Add":{"text":" : (∀ k, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4618"}},{"Add":{"text":" (if m1 !! k is Some v then Φ k v else emp) ⊢ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4679"}},{"Add":{"text":" (if m2 !! k is Some v then Ψ k v else emp))","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4736"}},{"Add":{"text":" -> ([∗ map] k ↦ v ∈ m1, Φ k v) ⊢ ([∗ map] k ↦ v ∈ m2, Ψ k v).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4822"}},{"Add":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4833"}},{"Add":{"text":" move: m2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4851"}},{"Add":{"text":" induction m1 as [|k v1 m1' fact1 IH1] using map_ind.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4912"}},{"Add":{"text":" - move=> m2 H. rewrite big_sepM_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:4959"}},{"Add":{"text":" induction m2 as [|k v2 m2' fact2 IH2] using map_ind.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5024"}},{"Add":{"text":" + by rewrite big_sepM_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5065"}},{"Add":{"text":" + rewrite big_sepM_insert; last exact fact2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5122"}},{"Add":{"text":" rewrite -(bi.emp_sep emp%I).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5167"}},{"Add":{"text":" apply: bi.sep_mono.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5203"}},{"Add":{"text":" * move: (H k) => H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5240"}},{"Add":{"text":" by rewrite lookup_empty lookup_insert in H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5305"}},{"Add":{"text":" * apply: IH2 => k'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5341"}},{"Add":{"text":" rewrite lookup_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5383"}},{"Add":{"text":" case: (decide (k = k')).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5428"}},{"Add":{"text":" -- move=><-. by rewrite fact2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5479"}},{"Add":{"text":" -- move=> neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5514"}},{"Add":{"text":" move: (H k').","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5552"}},{"Add":{"text":" by rewrite lookup_empty lookup_insert_ne.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5618"}}],"del_contents":[{"Del":{"text":"Lemma bind_spec {Σ} var (c : context Σ)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3620"}},{"Del":{"text":" : match ctx_uses var c with","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3652"}},{"Del":{"text":" | None => prop_of_ctx (bind var c) ⊢ prop_of_ctx c","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3713"}},{"Del":{"text":" | Some (uses, P, constraints) => ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3755"}},{"Del":{"text":" constraints -> ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3783"}},{"Del":{"text":" prop_of_ctx (bind var c) ∗ ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3825"}},{"Del":{"text":" (match uses with One => P | Many => □P end) ⊢ ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3888"}},{"Del":{"text":" prop_of_ctx c","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3914"}},{"Del":{"text":" end.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3923"}},{"Del":{"text":"Proof.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:3930"}},{"Del":{"text":" have: ∀ u (P : iProp Σ), □ P ⊢ match u with One => P | Many => □ P end.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4015"}},{"Del":{"text":" { case. apply: bi.intuitionistically_elim. done. }","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4070"}},{"Del":{"text":" move=> lemma1.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4089"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":181,"ins":{"up_context":[{"change":2,"pos":4091}],"down_context":[{"change":2,"pos":4246}],"flag":"BLOCK","start":5620,"end":5698,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":4091},"to":{"change":2,"start":4091,"end":4246},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" - move=> m2 H.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5642"}},{"Add":{"text":" rewrite big_sepM_insert; last exact fact1.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5697"}}],"del_contents":[{"Del":{"text":" have: ∀ u (P : iProp Σ), match u with One => P | Many => □ P end ⊢ P.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4171"}},{"Del":{"text":" { case. done. apply: bi.intuitionistically_elim. }","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4226"}},{"Del":{"text":" move=> lemma2.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4245"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":184,"ins":{"up_context":[{"change":2,"pos":4247}],"down_context":[{"change":2,"pos":6631}],"flag":"BLOCK","start":5699,"end":6309,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":4247},"to":{"change":2,"start":4247,"end":6631},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" apply: transitivity.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5731"}},{"Add":{"text":" { ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5746"}},{"Add":{"text":" apply: bi.sep_mono.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5782"}},{"Add":{"text":" - move: (H k) => H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5819"}},{"Add":{"text":" rewrite lookup_insert in H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5868"}},{"Add":{"text":" exact: H'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5899"}},{"Add":{"text":" - apply: (IH1 (delete k m2)) => k'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5951"}},{"Add":{"text":" case: (decide (k = k')).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:5996"}},{"Add":{"text":" + move=><-. by rewrite fact1 lookup_delete.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6060"}},{"Add":{"text":" + move=> neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6094"}},{"Add":{"text":" rewrite lookup_delete_ne; last exact neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6160"}},{"Add":{"text":" move: (H k').","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6198"}},{"Add":{"text":" rewrite lookup_insert_ne; last exact neq.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6264"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6294"}},{"Add":{"text":" }","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6308"}}],"del_contents":[{"Del":{"text":" elim c; simpl.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4265"}},{"Del":{"text":" - done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4277"}},{"Del":{"text":" - move=> var' P.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4298"}},{"Del":{"text":" case: (decide (var = var')).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4335"}},{"Del":{"text":" + by rewrite bi.emp_sep.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4368"}},{"Del":{"text":" + done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4384"}},{"Del":{"text":" - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4458"}},{"Del":{"text":" move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4534"}},{"Del":{"text":" simpl; rewrite c_and_spec; simpl;","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4576"}},{"Del":{"text":" [ move=>[/H1 w1 [/H2 w2 eq]] ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4614"}},{"Del":{"text":" | move: H2 => w2 /H1 w1 ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4647"}},{"Del":{"text":" | move: H1 => w1 /H2 w2 ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4680"}},{"Del":{"text":" | move: H1 H2 => w1 w2","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4711"}},{"Del":{"text":" ];","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4722"}},{"Del":{"text":" (apply: transitivity; last (apply: bi.and_mono; [apply: w1 | apply: w2])).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4805"}},{"Del":{"text":" + rewrite eq.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4827"}},{"Del":{"text":" apply: transitivity; first apply: bi.sep_and_r.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4887"}},{"Del":{"text":" apply: bi.and_mono; apply: bi.sep_mono_r.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4941"}},{"Del":{"text":" * case u1; last done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:4975"}},{"Del":{"text":" apply: transitivity; last apply: (lemma2 u2).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5037"}},{"Del":{"text":" by case u2.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5065"}},{"Del":{"text":" * case u2; last by case u1.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5105"}},{"Del":{"text":" apply: transitivity; last apply: (lemma2 u1).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5167"}},{"Del":{"text":" by case u1.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5195"}},{"Del":{"text":" + apply: transitivity; first apply: bi.sep_and_r.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5257"}},{"Del":{"text":" apply: bi.and_mono; first done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5301"}},{"Del":{"text":" rewrite -{2}[prop_of_ctx _]bi.sep_emp.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5352"}},{"Del":{"text":" apply: bi.sep_mono; first done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5396"}},{"Del":{"text":" apply: bi.True_intro.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5430"}},{"Del":{"text":" + apply: transitivity; first apply: bi.sep_and_r.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5488"}},{"Del":{"text":" apply: bi.and_mono; last done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5531"}},{"Del":{"text":" rewrite -{2}[prop_of_ctx _]bi.sep_emp.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5582"}},{"Del":{"text":" apply: bi.sep_mono; first done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5626"}},{"Del":{"text":" apply: bi.True_intro.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5660"}},{"Del":{"text":" + done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5676"}},{"Del":{"text":" - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5750"}},{"Del":{"text":" move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5826"}},{"Del":{"text":" simpl; rewrite c_sep_spec; simpl;","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5868"}},{"Del":{"text":" [ move=>[/H1 w1 [/H2 w2 eq]] ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5906"}},{"Del":{"text":" | move: H2 => w2 /H1 w1 ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5939"}},{"Del":{"text":" | move: H1 => w1 /H2 w2 ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:5972"}},{"Del":{"text":" | move: H1 H2 => w1 w2","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6003"}},{"Del":{"text":" ];","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6014"}},{"Del":{"text":" (apply: transitivity; last (apply: bi.sep_mono; [apply: w1 | apply: w2])).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6097"}},{"Del":{"text":" + apply: transitivity; ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6129"}},{"Del":{"text":" last (apply: bi.sep_mono; apply: bi.sep_mono_r; apply: lemma1).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6205"}},{"Del":{"text":" rewrite eq {1}bi.intuitionistically_sep_dup.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6262"}},{"Del":{"text":" rewrite bi.sep_assoc bi.sep_assoc; apply: bi.sep_mono_l.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6331"}},{"Del":{"text":" rewrite -bi.sep_assoc -bi.sep_assoc; apply: bi.sep_mono_r.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6402"}},{"Del":{"text":" by rewrite bi.sep_comm.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6438"}},{"Del":{"text":" + by rewrite ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6460"}},{"Del":{"text":" -bi.sep_assoc ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6487"}},{"Del":{"text":" [(prop_of_ctx (bind var c2) ∗ _)%I]bi.sep_comm","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6548"}},{"Del":{"text":" bi.sep_assoc.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6574"}},{"Del":{"text":" + by rewrite bi.sep_assoc.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6609"}},{"Del":{"text":" + done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6625"}},{"Del":{"text":"Qed.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6630"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":200,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":6636}],"down_context":[{"change":2,"pos":6636}],"flag":"BLOCK","start":6310,"end":6497,"inode":{"change":3,"pos":53}}},"contents":[{"Add":{"text":" have: m2 !! k = m2 !! k by []; case: {-1}(m2 !! k) => [v2|] fact2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6388"}},{"Add":{"text":" + by rewrite (big_sepM_delete _ m2).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6437"}},{"Add":{"text":" + by rewrite bi.emp_sep delete_notin.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6487"}},{"Add":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6496"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":205,"ins":{"up_context":[{"change":2,"pos":6637}],"down_context":[{"change":2,"pos":7306}],"flag":"BLOCK","start":6498,"end":13371,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":6637},"to":{"change":2,"start":6637,"end":7306},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6498"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6499"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6500"}},{"Add":{"text":" Definition sep {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6580"}},{"Add":{"text":" Constraints := Constraints c1 ∧ Constraints c2;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6638"}},{"Add":{"text":" Variables := union_with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6670"}},{"Add":{"text":" (λ '(P, u, c1) '(Q, v, c2), Some (P, uses_sep u v, c1 ∧ c2 ∧ P = Q)) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6757"}},{"Add":{"text":" (Variables c1) (Variables c2);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6800"}},{"Add":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6808"}},{"Add":{"text":" Theorem sep_spec {Σ} (c1 c2 : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6855"}},{"Add":{"text":" : prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6907"}},{"Add":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6918"}},{"Add":{"text":" rewrite /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6941"}},{"Add":{"text":" apply: bi.exist_elim; move => [w1 w2].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:6988"}},{"Add":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7044"}},{"Add":{"text":" rewrite bi.sep_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7100"}},{"Add":{"text":" clear w1 w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7121"}},{"Add":{"text":" ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7130"}},{"Add":{"text":" apply: transitivity; last (","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7166"}},{"Add":{"text":" apply: bi.sep_mono;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7198"}},{"Add":{"text":" [ apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7236"}},{"Add":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7262"}},{"Add":{"text":" if Variables c1 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7332"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7402"}},{"Add":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7437"}},{"Add":{"text":" (Variables (sep c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7483"}},{"Add":{"text":" | apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7521"}},{"Add":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7547"}},{"Add":{"text":" if Variables c2 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7617"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7687"}},{"Add":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7722"}},{"Add":{"text":" (Variables (sep c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7768"}},{"Add":{"text":" ]","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7782"}},{"Add":{"text":" ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7793"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7794"}},{"Add":{"text":" - rewrite -big_sepM_sep.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7827"}},{"Add":{"text":" apply: big_sepM_mono => k [[P u] constraints] fact.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7891"}},{"Add":{"text":" apply: bi.exist_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7925"}},{"Add":{"text":" move: fact; rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:7976"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8044"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8112"}},{"Add":{"text":" simpl; last done;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8142"}},{"Add":{"text":" move=>w; injection w; clear w;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8185"}},{"Add":{"text":" move=> <-<-<- w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8214"}},{"Add":{"text":" + move: w => [w1 [w2 <-]].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8253"}},{"Add":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8317"}},{"Add":{"text":" rewrite bi.sep_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8381"}},{"Add":{"text":" apply: uses_sep_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8419"}},{"Add":{"text":" + by rewrite bi.sep_emp; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8480"}},{"Add":{"text":" + by rewrite bi.emp_sep; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8541"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8578"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8646"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8714"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8732"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8769"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8837"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8905"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8923"}},{"Add":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8932"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:8933"}},{"Add":{"text":" Definition and {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9013"}},{"Add":{"text":" Constraints := Constraints c1 ∧ Constraints c2;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9071"}},{"Add":{"text":" Variables := union_with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9103"}},{"Add":{"text":" (λ '(P, u, c1) '(Q, v, c2), Some (P, uses_and u v, c1 ∧ c2 ∧ P = Q)) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9190"}},{"Add":{"text":" (Variables c1) (Variables c2);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9233"}},{"Add":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9241"}},{"Add":{"text":" Theorem and_spec {Σ} (c1 c2 : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9288"}},{"Add":{"text":" : prop (and c1 c2) ⊢ prop c1 ∧ prop c2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9340"}},{"Add":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9351"}},{"Add":{"text":" rewrite /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9374"}},{"Add":{"text":" apply: bi.exist_elim; move => [w1 w2].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9421"}},{"Add":{"text":" rewrite bi.and_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9477"}},{"Add":{"text":" rewrite bi.and_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9533"}},{"Add":{"text":" clear w1 w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9554"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9555"}},{"Add":{"text":" apply: transitivity; last (","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9591"}},{"Add":{"text":" apply: bi.and_mono;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9623"}},{"Add":{"text":" [ apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9661"}},{"Add":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9687"}},{"Add":{"text":" if Variables c1 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9757"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9827"}},{"Add":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9862"}},{"Add":{"text":" (Variables (and c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9908"}},{"Add":{"text":" | apply: (big_sepM_hetero","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9946"}},{"Add":{"text":" (λ k _, ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:9972"}},{"Add":{"text":" if Variables c2 !! k is Some (P, u, constraints) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10042"}},{"Add":{"text":" then ∃ _ : (constraints : Prop), uses_prop u P ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10112"}},{"Add":{"text":" else emp)%I _ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10147"}},{"Add":{"text":" (Variables (and c1 c2))) => k","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10193"}},{"Add":{"text":" ]","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10207"}},{"Add":{"text":" ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10218"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10219"}},{"Add":{"text":" - rewrite -big_sepM_and. ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10253"}},{"Add":{"text":" apply: big_sepM_mono => k [[P u] constraints] fact.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10317"}},{"Add":{"text":" apply: bi.exist_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10351"}},{"Add":{"text":" move: fact; rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10402"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10470"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10538"}},{"Add":{"text":" simpl; last done;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10568"}},{"Add":{"text":" move=>w; injection w; clear w;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10611"}},{"Add":{"text":" move=> <-<-<- w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10640"}},{"Add":{"text":" + move: w => [w1 [w2 <-]].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10679"}},{"Add":{"text":" rewrite bi.and_exist_l; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10743"}},{"Add":{"text":" rewrite bi.and_exist_r; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10807"}},{"Add":{"text":" apply: uses_and_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10845"}},{"Add":{"text":" + by rewrite bi.and_True; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10907"}},{"Add":{"text":" + by rewrite bi.True_and; apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:10969"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11006"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11074"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11142"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11160"}},{"Add":{"text":" - rewrite lookup_union_with.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11197"}},{"Add":{"text":" case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11265"}},{"Add":{"text":" case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11333"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11351"}},{"Add":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11360"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11361"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11362"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11363"}},{"Add":{"text":" Definition bind {Σ} (var : string) (ctx : context Σ) : context Σ := {|","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11441"}},{"Add":{"text":" Variables := delete var (Variables ctx);","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11490"}},{"Add":{"text":" Constraints := Constraints ctx ∧ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11534"}},{"Add":{"text":" if Variables ctx !! var is Some (_, _, constraints)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11598"}},{"Add":{"text":" then constraints ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11628"}},{"Add":{"text":" else True;","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11651"}},{"Add":{"text":" |}.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11659"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11660"}},{"Add":{"text":" Definition lookup {Σ} (var : string) (ctx : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11721"}},{"Add":{"text":" : option (iProp Σ * uses)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11756"}},{"Add":{"text":" := option_map fst (Variables ctx !! var).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11802"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11803"}},{"Add":{"text":" Theorem bind_spec {Σ} var (c : context Σ)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11851"}},{"Add":{"text":" : match lookup var c with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11885"}},{"Add":{"text":" | None => emp","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11911"}},{"Add":{"text":" | Some (P, uses) => (uses_prop uses P)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:11962"}},{"Add":{"text":" end ∗ prop (bind var c) ⊢ ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12001"}},{"Add":{"text":" prop c.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12017"}},{"Add":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12028"}},{"Add":{"text":" rewrite /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12051"}},{"Add":{"text":" rewrite bi.sep_exist_l; apply: bi.exist_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12105"}},{"Add":{"text":" move=> [w1 w2].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12129"}},{"Add":{"text":" apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12161"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12162"}},{"Add":{"text":" rewrite /lookup.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12187"}},{"Add":{"text":" move: w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12205"}},{"Add":{"text":" have: Variables c !! var = Variables c !! var by [];","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12266"}},{"Add":{"text":" case: {-1}(Variables c !! var) => [[[P u] constraints]|] fact w2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12344"}},{"Add":{"text":" - simpl.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12361"}},{"Add":{"text":" rewrite (big_sepM_delete _ (Variables c)); last exact fact.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12433"}},{"Add":{"text":" rewrite bi.sep_exist_r. apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12493"}},{"Add":{"text":" done.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12511"}},{"Add":{"text":" - simpl. ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12529"}},{"Add":{"text":" by rewrite bi.emp_sep delete_notin.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12577"}},{"Add":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12586"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12587"}},{"Add":{"text":" Definition toplevel {Σ} (ctx : context Σ) : Prop :=","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12645"}},{"Add":{"text":" if decide (Variables ctx = ∅) ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12686"}},{"Add":{"text":" then Constraints ctx","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12715"}},{"Add":{"text":" else error (","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12736"}},{"Add":{"text":" \"Variables not in scope.\", ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12776"}},{"Add":{"text":" map fst (map_to_list (Variables ctx))","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12826"}},{"Add":{"text":" ).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12837"}},{"Add":{"text":" Theorem toplevel_spec {Σ} (ctx : context Σ) :","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12889"}},{"Add":{"text":" toplevel ctx -> ⊢ prop ctx.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12927"}},{"Add":{"text":" Proof.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12938"}},{"Add":{"text":" rewrite /toplevel /prop.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:12971"}},{"Add":{"text":" case: (decide (Variables ctx = ∅)) => [-> | _] w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13031"}},{"Add":{"text":" - apply: bi.exist_intro'.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13065"}},{"Add":{"text":" by rewrite big_sepM_empty.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13104"}},{"Add":{"text":" - by apply: error_elim.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13136"}},{"Add":{"text":" Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13145"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13146"}},{"Add":{"text":"End context.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13159"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13160"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13161"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13162"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13163"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13164"}},{"Add":{"text":"Inductive expr {Σ : gFunctors} : iProp Σ -> Type :=","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13218"}},{"Add":{"text":" | Var {T} : string -> expr T","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13251"}},{"Add":{"text":" | Lam {T1 T2} : string -> expr T2 -> expr (T1 -∗ T2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13310"}},{"Add":{"text":" | Pair {T1 T2} : expr T1 -> expr T2 -> expr (T1 ∗ T2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13370"}}],"del_contents":[{"Del":{"text":"Inductive expr {Σ : gFunctors} : context Σ -> iProp Σ -> Type :=","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6704"}},{"Del":{"text":" | Pair {c1 c2 T1 T2} : expr c1 T1 -> expr c2 T2 -> expr (c_sep c1 c2) (T1 ∗ T2)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6790"}},{"Del":{"text":" | Var {T} : ∀ var, expr (CVar var T) T","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6835"}},{"Del":{"text":" | Lam {ctx T1 T2} ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6858"}},{"Del":{"text":" : ∀ var {constraints : match ctx_uses var ctx with","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6919"}},{"Del":{"text":" | None => True","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6946"}},{"Del":{"text":" | Some (uses, type, constraints) =>","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:6994"}},{"Del":{"text":" constraints ∧ type = T1 ∧ match uses with ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7057"}},{"Del":{"text":" | Many => error ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7094"}},{"Del":{"text":" ( \"A linear variable was used multiple times.\", var )","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7172"}},{"Del":{"text":" | One => True","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7206"}},{"Del":{"text":" end","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7226"}},{"Del":{"text":" end },","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7241"}},{"Del":{"text":" expr ctx T2 ->","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7264"}},{"Del":{"text":" expr (bind var ctx) (T1 -∗ T2)","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7305"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":388,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7308}],"down_context":[{"change":2,"pos":7308}],"flag":"BLOCK","start":13372,"end":13865,"inode":{"change":3,"pos":53}}},"contents":[{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13372"}},{"Add":{"text":"Fixpoint check_expr {Σ} {type : iProp Σ} (e : expr type) : context.context Σ := match e with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13468"}},{"Add":{"text":" | Var var => context.var var type","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13506"}},{"Add":{"text":" | @Lam _ T1 T2 var e =>","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13534"}},{"Add":{"text":" let ctx := check_expr e in","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13569"}},{"Add":{"text":" context.constrain","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13595"}},{"Add":{"text":" (match context.lookup var ctx with","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13642"}},{"Add":{"text":" | Some (T, uses) => T = T1 ∧ uses = One","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13700"}},{"Add":{"text":" | None => True","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13731"}},{"Add":{"text":" end)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13748"}},{"Add":{"text":" (context.bind var (check_expr e))","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13794"}},{"Add":{"text":" | Pair e1 e2 => context.sep (check_expr e1) (check_expr e2)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13858"}},{"Add":{"text":"end.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13863"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13864"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":403,"ins":{"up_context":[{"change":2,"pos":7309}],"down_context":[{"change":2,"pos":7403}],"flag":"BLOCK","start":13866,"end":13972,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":7309},"to":{"change":2,"start":7309,"end":7403},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Lemma check_expr_spec {Σ} (type : iProp Σ) (e : expr type) : ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13929"}},{"Add":{"text":" context.prop (check_expr e) ⊢ type.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13971"}}],"del_contents":[{"Del":{"text":"Lemma check_expr {Σ ctx} (type : iProp Σ) : ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7355"}},{"Del":{"text":" expr ctx type -> prop_of_ctx ctx ⊢ type.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7402"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":406,"ins":{"up_context":[{"change":2,"pos":7410}],"down_context":[{"change":2,"pos":7502}],"flag":"BLOCK","start":13973,"end":14612,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":7410},"to":{"change":2,"start":7410,"end":7502},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" elim e; simpl.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:13991"}},{"Add":{"text":" - move=> T var. apply: context.var_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14036"}},{"Add":{"text":" - move=> T1 T2 var body H.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14067"}},{"Add":{"text":" apply: transitivity; first apply: context.constrain_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14133"}},{"Add":{"text":" apply: bi.exist_elim => w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14168"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14169"}},{"Add":{"text":" apply: bi.wand_intro_r.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14201"}},{"Add":{"text":" apply: transitivity; last apply: H.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14245"}},{"Add":{"text":" apply: transitivity; last apply: (context.bind_spec var).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14311"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14312"}},{"Add":{"text":" rewrite {1}bi.sep_comm.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14344"}},{"Add":{"text":" apply: bi.sep_mono_l.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14374"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14375"}},{"Add":{"text":" move: w; case: (context.lookup var (check_expr body)) => [[P u]|].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14450"}},{"Add":{"text":" + by move=>[->->].","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14477"}},{"Add":{"text":" + move=>[]. apply: bi.True_intro.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14519"}},{"Add":{"text":" - move=> T1 T2 e1 H1 e2 H2.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14551"}},{"Add":{"text":" apply: transitivity; first apply: context.sep_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14611"}}],"del_contents":[{"Del":{"text":" elim.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7419"}},{"Del":{"text":" - move=> ctx1 ctx2 type1 type2 e1 fact1 e2 fact2.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7473"}},{"Del":{"text":" rewrite c_sep_spec.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7501"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":425,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":7533},"to":{"change":2,"start":7533,"end":8171},"introduced_by":2}],"inode":{"change":3,"pos":53}}},"contents":[{"Del":{"text":" - done.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7544"}},{"Del":{"text":" - move=> ctx1 type1 type2 var w e fact1.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7589"}},{"Del":{"text":" move: (bind_spec var ctx1) w.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7627"}},{"Del":{"text":" case: (ctx_uses var ctx1) => [[[uses P] constraint]|].","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7690"}},{"Del":{"text":" + case uses; last (move=> _ [_ [_ err]]; apply: (error_elim err)).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7765"}},{"Del":{"text":" move=> H2 [/H2 fact2 [<- []]].","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7808"}},{"Del":{"text":" apply: bi.wand_intro_r.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7844"}},{"Del":{"text":" apply: transitivity.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7877"}},{"Del":{"text":" * apply: fact2.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7905"}},{"Del":{"text":" * apply: fact1.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7933"}},{"Del":{"text":" + move=> fact2 [].","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7960"}},{"Del":{"text":" apply: bi.wand_intro_r.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:7996"}},{"Del":{"text":" rewrite -[type2]bi.sep_emp.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8036"}},{"Del":{"text":" apply: bi.sep_mono.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8068"}},{"Del":{"text":" * apply: transitivity; [apply: fact2 | apply: fact1].","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8134"}},{"Del":{"text":" * apply: bi.True_intro.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8170"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":427,"ins":{"up_context":[{"change":2,"pos":8177}],"down_context":[{"change":2,"pos":8263}],"flag":"BLOCK","start":14613,"end":14827,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":8177},"to":{"change":2,"start":8177,"end":8263},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Definition check_program {Σ} {type : iProp Σ} (e : expr type) : Prop :=","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14686"}},{"Add":{"text":" context.toplevel (check_expr e).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14723"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14724"}},{"Add":{"text":"Theorem check_program_spec {Σ} {type : iProp Σ} (e : expr type) : ","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14793"}},{"Add":{"text":" check_program e -> ⊢ type.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14826"}}],"del_contents":[{"Del":{"text":"Theorem check_program {Σ} (type : iProp Σ) : ","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8224"}},{"Del":{"text":" expr (CEmpty _) type -> ⊢ type.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8262"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":433,"ins":{"up_context":[{"change":2,"pos":8270}],"down_context":[{"change":2,"pos":8293}],"flag":"BLOCK","start":14828,"end":15102,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":8270},"to":{"change":2,"start":8270,"end":8293},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" move=> w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14841"}},{"Add":{"text":" apply: transitivity.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14866"}},{"Add":{"text":" - apply: context.toplevel_spec w.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14904"}},{"Add":{"text":" - apply: check_expr_spec.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14934"}},{"Add":{"text":"Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14939"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14940"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14941"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14942"}},{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14943"}},{"Add":{"text":"(* Example Proof. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:14964"}},{"Add":{"text":"Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15010"}},{"Add":{"text":" move=> Σ P Q.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15029"}},{"Add":{"text":" apply: (check_program_spec (Lam \"x\" (Var \"x\"))).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15082"}},{"Add":{"text":" by vm_compute.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15101"}}],"del_contents":[{"Del":{"text":" exact: check_expr.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8292"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":450,"ins":{"up_context":[{"change":2,"pos":8320}],"down_context":[{"change":2,"pos":8382}],"flag":"BLOCK","start":15103,"end":15162,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":8320},"to":{"change":2,"start":8320,"end":8382},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":"Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15161"}}],"del_contents":[{"Del":{"text":"Goal forall {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8381"}}]}},{"Replacement":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":452,"ins":{"up_context":[{"change":2,"pos":8401}],"down_context":[{"change":2,"pos":8479}],"flag":"BLOCK","start":15163,"end":15262,"inode":{"change":3,"pos":53}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":8401},"to":{"change":2,"start":8401,"end":8479},"introduced_by":2}],"inode":{"change":3,"pos":53}},"ins_contents":[{"Add":{"text":" apply: (check_program_spec (Lam \"x\" (Lam \"y\" (Pair (Var \"y\") (Var \"x\"))))).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15242"}},{"Add":{"text":" by vm_compute.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15261"}}],"del_contents":[{"Del":{"text":" by apply: (check_program (Lam \"x\" (Lam \"y\" (Pair (Var \"y\") (Var \"x\"))))).","pos":"J6DASJOO4LMJJVN6QOBHPC6GHVIY2CFFYJ75AJL3D6H3JRC4MPXAC:8478"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":456,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":8485}],"down_context":[{"change":2,"pos":8485}],"flag":"BLOCK","start":15263,"end":15512,"inode":{"change":3,"pos":53}}},"contents":[{"Add":{"text":"(* Example Proof. *)","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15283"}},{"Add":{"text":"Goal ∀ {Σ} (P Q R : iProp Σ), ⊢ P -∗ Q -∗ R -∗ (R ∗ Q) ∗ P.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15359"}},{"Add":{"text":" move=> Σ P Q R.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15380"}},{"Add":{"text":" apply: (check_program_spec (Lam \"x\" (Lam \"y\" (Lam \"z\" (Pair (Pair (Var \"z\") (Var \"y\")) (Var \"x\")))))).","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15487"}},{"Add":{"text":" by vm_compute.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15506"}},{"Add":{"text":"Qed.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15511"}}]}},{"Edit":{"inode":{"change":3,"pos":53},"path":"theories/lang.v","line":464,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":8487}],"down_context":[],"flag":"BLOCK","start":15513,"end":15514,"inode":{"change":3,"pos":53}}},"contents":[{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15513"}}]}},{"Edit":{"inode":{"change":2,"pos":8520},"path":"TODO.md","line":4,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":8551}],"down_context":[{"change":2,"pos":8551}],"flag":"BLOCK","start":15515,"end":15545,"inode":{"change":2,"pos":8520}}},"contents":[{"Add":{"text":"","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15515"}},{"Add":{"text":"- Fix the performance issue.","pos":"TZUF72D63PSGMASMQQTWQAUGEAPVMSTR7LQVKQSR5VRUVDGUWNPQC:15544"}}]}}],"owner":"finegeometer","repo":"iris-curry-howard","token":"KI+YZ9qzVAUxe+K5uRIiiDyzvui3GRhmnHSTCK7UnmI=","login":null}

…

Dependencies

Change contents

Review