1:"/_next/static/chunks/37p22ce5mxv7g.js" 2:"/_next/static/chunks/0z7qrcr6nv___.js" 3:"/_next/static/chunks/1714lgjf11pif.js" 4:"/_next/static/chunks/0s6ei21j90j07.js" 5:"/_next/static/chunks/0iifrvd3blsb8.js" 6:"/_next/static/chunks/44k_miop-abi_.js" 7:"/_next/static/chunks/0ldx9jrtnu57t.js" 8:"/_next/static/chunks/0w7u7n_j9kh34.js" 9:"LoadingBoundaryProvider" a:I[534085,["$1","$2","$3","$4","$5","$6","$7","$8"],"$9"] b:"$Sreact.fragment" c:I[993764,["$1","$2","$3","$4","$5","$6","$7","$8"],"Providers"] d:"LanguageProvider" e:I[195198,["$1","$2","$3","$4","$5","$6","$7","$8"],"$d"] f:I[834147,["$1","$2","$3","$4","$5","$6","$7","$8"],"EnsureAccount"] 10:I[658451,["$1","$2","$3","$4","$5","$6","$7","$8"],"AppHeader"] 11:I[146007,["$1","$2","$3","$4","$5","$6","$7","$8"],"AccessGate"] 12:I[534085,["$1","$2","$3","$4","$5","$6","$7","$8"],"default"] 13:"/_next/static/chunks/22oey3oj8h8dz.js" 14:I[763372,["$1","$2","$3","$4","$5","$6","$7","$8","$13"],"default"] 15:I[443948,["$1","$2","$3","$4","$5","$6","$7","$8"],"default"] 19:"/_next/static/chunks/0h9kteqepbrxb.js" 1a:I[542186,["$1","$2","$3","$4","$5","$6","$7","$8","$19"],"DocsPage"] 1e:"ViewportBoundary" 1f:I[485605,["$1","$2","$3","$4","$5","$6","$7","$8"],"$1e"] 21:"MetadataBoundary" 22:I[485605,["$1","$2","$3","$4","$5","$6","$7","$8"],"$21"] 23:"$Sreact.suspense" 25:I[329733,["$1","$2","$3","$4","$5","$6","$7","$8"],"default",1] :HL["/_next/static/chunks/0yjrr8awe4cs_.css","style"] :HL["/_next/static/chunks/2gan83usjgz4q.css","style"] :HL["/_next/static/chunks/1bub626g5au1k.css","style"] :HL["/_next/static/chunks/41omn5azlzymz.css","style"] :HL["/_next/static/chunks/21lieq632gtrh.css","style"] 17:X 1b:T37041,# Internal service API Console and Logic call the Parsimony API at `https://api.p7y.ai` in production and `https://parsimony-api-dev-chirbppamq-uc.a.run.app` in dev. Every route below requires an internal role: send the signed-in person's Firebase ID token in `Authorization: Bearer …`. External people receive task products instead — see the docs for Proof, Meaning and Action. The API's [frontend integration guide](https://github.com/Pangeon-Corp/parsimony_api/blob/main/docs/FRONTEND_INTEGRATION.md) is the authoritative contract. Generate client types from the dev `/openapi.json`; production hides OpenAPI. ## Logic | Route | Use | | --- | --- | | `POST /sheaf/run` | Run a SHEAF program: every logic, knowledge-base and stored-tree operation. | | `GET /config` | Parser configuration and the SHEAF operation inventory (`sheaf_operations`). | Add `?deterministic=true` to `/sheaf/run` for the same bindings from the same program and inputs on any machine. See the [SHEAF reference](https://github.com/Pangeon-Corp/parsimony_api/blob/main/SHEAF/reference.md). ### Certified answers `prove k t` answers with a record. `found` is true only for a proof. The `search_status` is one of: | Status | Meaning | | --- | --- | | `proved` | The premises entail the target. | | `disproved` | The premises refute the target (they entail its negation). `found` is false. | | `saturated` | The search ran out of clauses to derive without a proof or a disproof. | | `budget_exhausted` | The search hit its clause or depth budget; nothing is known. | A `proved` or `disproved` answer carries a `certificate` and a `verdict`. The certificate (`sheaf/certificate/1`) lists every premise's tree, its canonical hash and its clauses, the goal's, and the resolution steps, each naming the two literals it resolved on. The verdict is the kernel's: `accepted`, the `answer`, the number of `steps`, and `derived`, the clause the kernel itself derived for each step. Nothing in the certificate is trusted: the kernel recomputes every hash, retranslates every tree and replays every step before it says `accepted`. `steps` in the record is that replay rendered as the chain of statements. The record also carries a `signature`: the API's Ed25519 JWS over the certificate's canonical hash and the verdict, made with the evidence key whose public keys are served at `/.well-known/jwks.json`, so a reader can keep a proof and check later that this API vouched for it. The format and the checks are documented in [`SHEAF/certificates.md`](https://github.com/Pangeon-Corp/parsimony_api/blob/main/SHEAF/certificates.md); the kernel's soundness is proved in Lean against its extracted code (`sheaf/spec`, `certificate_sound`). To check a certificate yourself, save the `certificate` value to a file and run the kernel's command-line front end, built from the private `parsimony_api` checkout with `make sheaf-build`: ``` sheaf/target/release/sheaf-check certificate.json ``` It prints the verdict; `accepted: false` comes with a `reason` such as `translation_mismatch` or `invalid_step`. ## What Lean proves about SHEAF SHEAF's kernel is written in Rust and translated to Lean with Aeneas; the semantics and the theorems below live in `sheaf/spec/` of the API repository and are checked by `make sheaf-kernel-lean` on every release. This page is generated from those files (`scripts/sheaf_proof_index.py`): each theorem's statement is shown as Lean, with its explanation in plain language above it. Proof bodies and kernel code are not shown. What the chain establishes, outermost first: an accepted certificate's premise formulas have no model together with the goal's clause-form formula (`certificate_sound`), so a `proved` answer means the premises entail the target and a `disproved` answer means they refute it; the formulas are what the translator computes from the trees, and the translator's operator layer, terms and atoms are proved to be what `SHEAF/semantics.md` says (`Translator`, `Terms`, `Atoms`). The one stated assumption is the hash discipline (`Consistent`); the remaining trusted parts are named in each module's header. 296 theorems across 21 modules; `sorry` count: 0. ### `Sheaf/Term.lean` **Terms, literals, clauses and substitution** These mirror `sheaf-kernel/src/first_order.rs`. A term is a variable, a tuple of terms, or an atom. Tuples are how constants, Skolem applications, participant groups and reified propositions are all written; the logic treats a tuple of arity `n` as the application of one `n`-ary tupling function, which is all resolution ever needs to know about them. Atoms and predicate symbols are opaque: the kernel compares them for equality and nothing else, so the development is parametric in their types `A` and `P`. The kernel instantiates both with its canonical JSON values (`SheafKernel.Substitution`). _Definitions only._ ### `Sheaf/Semantics.lean` **Tarski semantics for terms, literals and clauses** A structure interprets tuples, atoms and predicate symbols over a domain. A valuation assigns domain elements to variable names. A clause is true in a structure when, for every valuation, some literal of it is true. #### `skolemName_subst` Which atoms write Skolem terms: a Skolem term is the tuple `[tag, name s, [args]]` (`SHEAF/semantics.md` §2), and it denotes the value of the witness function `s` at the args, not a tuple. -/ class SkolemAtoms (A : Type) where tag : A name : String → A name_injective : Function.Injective name /-- An interpretation: a nonempty domain with interpretations of tupling, atoms, predicates and Skolem witness functions. Tupling of every arity is one function on lists. -/ structure Structure (P A : Type) where D : Type inhabited : Inhabited D tup : List D → D atom : A → D pred : P → List D → Prop skolem : String → List D → D variable {A P : Type} /-- A valuation of variable names. -/ abbrev Valuation (M : Structure P A) := String → M.D open Classical in /-- The Skolem witness a term list names, if it has the Skolem shape. -/ noncomputable def skolemName [SkolemAtoms A] : List (Term A) → Option (String × List (Term A)) | [.atom t, .atom n, .node args] => if h : t = SkolemAtoms.tag ∧ ∃ s, n = SkolemAtoms.name s then some (Classical.choose h.2, args) else none | _ => none theorem sizeOf_lt_of_skolemName [SkolemAtoms A] {cs : List (Term A)} {s : String} {args : List (Term A)} (h : skolemName cs = some (s, args)) {x : Term A} (hx : x ∈ args) : sizeOf x < sizeOf cs := by unfold skolemName at h split at h · split at h · simp only [Option.some.injEq, Prod.mk.injEq] at h obtain ⟨_, h2⟩ := h subst h2 subst_vars have := List.sizeOf_lt_of_mem hx simp omega · exact absurd h (by simp) · exact absurd h (by simp) /-- A term is a variable. -/ def Term.isVar : Term A → Prop | .var _ => True | .node _ => False | .atom _ => False /-- Well-formed terms: no three-element tuple has a variable as a direct element. Substitution can then never turn a tuple into the Skolem shape or out of it, so the value of a substituted term is the value of the term under the induced valuation (`Term.eval_subst`). The translator never writes such a tuple, and the kernel checks every clause it registers. -/ inductive Term.WF : Term A → Prop | var (x : String) : Term.WF (.var x) | atom (a : A) : Term.WF (.atom a) | node (cs : List (Term A)) (hlen : cs.length = 3 → ∀ c ∈ cs, ¬ c.isVar) (h : ∀ c ∈ cs, Term.WF c) : Term.WF (.node cs) theorem Term.WF.elements {cs : List (Term A)} (h : Term.WF (.node cs)) : ∀ c ∈ cs, Term.WF c := by cases h with | node _ _ h => exact h theorem Term.WF.heads {cs : List (Term A)} (h : Term.WF (.node cs)) : cs.length = 3 → ∀ c ∈ cs, ¬ c.isVar := by cases h with | node _ hlen _ => exact hlen /-- The literals and clauses whose terms are all well-formed. -/ def Literal.WF (l : Literal P A) : Prop := ∀ t ∈ l.terms, Term.WF t def Clause.WF (c : Clause P A) : Prop := ∀ l ∈ c, Literal.WF l /-- The value of a term. A tuple of the Skolem shape is the witness function at its arguments; any other tuple is the tupling function at its elements. -/ noncomputable def Term.eval [SkolemAtoms A] (M : Structure P A) (v : Valuation M) : Term A → M.D | .var x => v x | .node cs => match h : skolemName cs with | some (s, args) => M.skolem s (args.attach.map (fun x => Term.eval M v x.val)) | none => M.tup (cs.attach.map (fun x => Term.eval M v x.val)) | .atom a => M.atom a termination_by t => sizeOf t decreasing_by · have := sizeOf_lt_of_skolemName h x.property simp_wf omega · have := List.sizeOf_lt_of_mem x.property simp_wf omega theorem Term.eval_var [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (x : String) : Term.eval M v (.var x) = v x := by rw [Term.eval] theorem Term.eval_atom [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (a : A) : Term.eval M v (.atom a) = M.atom a := by rw [Term.eval] theorem Term.eval_node [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (cs : List (Term A)) : Term.eval M v (.node cs) = match skolemName cs with | some (s, args) => M.skolem s (args.map (Term.eval M v)) | none => M.tup (cs.map (Term.eval M v)) := by rw [Term.eval] split <;> rename_i heq <;> simp [heq] /-- The truth of a literal under a valuation. -/ def Literal.sat [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (l : Literal P A) : Prop := if l.positive then M.pred l.pred (l.terms.map (Term.eval M v)) else ¬ M.pred l.pred (l.terms.map (Term.eval M v)) /-- A clause holds under a valuation when one of its literals does. -/ def Clause.satAt [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (c : Clause P A) : Prop := ∃ l ∈ c, l.sat M v /-- A clause is true in a structure when it holds under every valuation (its variables are implicitly universally quantified). -/ def Clause.true [SkolemAtoms A] (M : Structure P A) (c : Clause P A) : Prop := ∀ v : Valuation M, c.satAt M v /-- The valuation obtained by evaluating a substitution's terms. -/ def Valuation.ofSubst [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (σ : Subst A) : Valuation M := fun x => match σ x with | some t => t.eval M v | none => v x /-- Substitution keeps a well-formed tuple's Skolem shape, and its name. ```lean theorem skolemName_subst [SkolemAtoms A] (σ : Subst A) (cs : List (Term A)) (hwf : Term.WF (.node cs)) : skolemName (cs.map (Term.subst σ)) = (skolemName cs).map (fun p => (p.1, p.2.map (Term.subst σ))) ``` #### `Term.eval_subst` The substitution lemma for terms: evaluating `t σ` under `v` is evaluating `t` under the valuation that sends each variable to the value of its image. ```lean theorem Term.eval_subst [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (σ : Subst A) : (t : Term A) → t.WF → (t.subst σ).eval M v = t.eval M (Valuation.ofSubst M v σ) | .var x, _ => by unfold Term.subst Valuation.ofSubst split <;> simp [*, Term.eval_var] | .node cs, hwf => by rw [Term.subst, Term.eval_node, Term.eval_node, skolemName_subst σ cs hwf] cases h : skolemName cs with | none => simp only [Option.map_none, List.map_map, Function.comp_def] congr 1 apply List.map_congr_left intro x hx exact Term.eval_subst M v σ x (hwf.elements x hx) | some p => obtain ⟨s, args⟩ ``` #### `Term.evalList_subst` The substitution lemma for lists of terms. ```lean theorem Term.evalList_subst [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (σ : Subst A) (cs : List (Term A)) (hwf : ∀ t ∈ cs, Term.WF t) : cs.map (fun t => (t.subst σ).eval M v) = cs.map (fun t => t.eval M (Valuation.ofSubst M v σ)) ``` #### `Literal.sat_subst` The substitution lemma for literals. ```lean theorem Literal.sat_subst [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (σ : Subst A) (l : Literal P A) (hwf : l.WF) : (l.subst σ).sat M v ↔ l.sat M (Valuation.ofSubst M v σ) ``` #### `Clause.true_subst` A true clause stays true under any substitution (an instance of a universal truth is true). ```lean theorem Clause.true_subst [SkolemAtoms A] (M : Structure P A) (c : Clause P A) (σ : Subst A) (hwf : c.WF) (h : c.true M) : (c.subst σ).true M ``` #### `Clause.true_of_subset` Truth depends only on which literals a clause has: a clause whose literals all occur in a true clause, and which has all of its literals, is true. More useful in the weaker form below. ```lean theorem Clause.true_of_subset [SkolemAtoms A] (M : Structure P A) (c d : Clause P A) (h : ∀ l ∈ c, l ∈ d) (hc : c.true M) : d.true M ``` ### `Sheaf/Formula.lean` **First-order formulas and their truth** The translator produces a closed first-order formula for each tree (`sheaf-kernel/src/clause_form.rs`, `SHEAF/semantics.md` §1 and §5); the clause form then turns it into clauses. These are the formulas, with the same connectives, and their Tarski truth in a structure under a valuation. `and` and `or` take lists, as the kernel's do; an empty `and` is true and an empty `or` false. #### `Formula.sat_atom` ```lean theorem Formula.sat_atom [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (p : P) (terms : List (Term A)) : Formula.sat M v (.atom p terms) ↔ M.pred p (terms.map (Term.eval M v)) ``` #### `Formula.sat_not` ```lean theorem Formula.sat_not [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (f : Formula P A) : Formula.sat M v (.not f) ↔ ¬ Formula.sat M v f ``` #### `Formula.sat_and` ```lean theorem Formula.sat_and [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (parts : List (Formula P A)) : Formula.sat M v (.and parts) ↔ ∀ f ∈ parts, Formula.sat M v f ``` #### `Formula.sat_or` ```lean theorem Formula.sat_or [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (parts : List (Formula P A)) : Formula.sat M v (.or parts) ↔ ∃ f ∈ parts, Formula.sat M v f ``` #### `Formula.sat_implies` ```lean theorem Formula.sat_implies [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (f g : Formula P A) : Formula.sat M v (.implies f g) ↔ (Formula.sat M v f → Formula.sat M v g) ``` #### `Formula.sat_all` ```lean theorem Formula.sat_all [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (x : String) (body : Formula P A) : Formula.sat M v (.all x body) ↔ ∀ d : M.D, Formula.sat M (v.update x d) body ``` #### `Formula.sat_exists` ```lean theorem Formula.sat_exists [SkolemAtoms A] (M : Structure P A) (v : Valuation M) (x : String) (body : Formula P A) : Formula.sat M v (.exists x body) ↔ ∃ d : M.D, Formula.sat M (v.update x d) body ``` ### `Sheaf/Skolem.lean` **Skolem witnesses** The clause form replaces an existential in positive position by a witness term `[tag, name, [universals]]` (`SHEAF/semantics.md` §5), which the semantics reads as a witness function at the universals' values (`Term.eval`). Here are the pieces the soundness proof needs: the witness term and its value; changing a structure's witness function for one name; which names a term or formula mentions, and that a term mentioning no changed name keeps its value; the free variables of terms and formulas, and that truth depends on a valuation only at the free variables; and substitution of free variables at the atoms, as the clause form applies it. #### `Term.eval_withSkolem` The witness term for Skolem name `s` over the universals `U`. -/ def witness (s : String) (U : List (Term A)) : Term A := .node [.atom SkolemAtoms.tag, .atom (SkolemAtoms.name s), .node U] theorem skolemName_witness (s : String) (U : List (Term A)) : skolemName [Term.atom SkolemAtoms.tag, Term.atom (SkolemAtoms.name s), Term.node U] = some (s, U) := by have h : (SkolemAtoms.tag : A) = SkolemAtoms.tag ∧ ∃ s', (SkolemAtoms.name s : A) = SkolemAtoms.name s' := ⟨rfl, s, rfl⟩ simp only [skolemName] rw [dif_pos h] simp only [Option.some.injEq, Prod.mk.injEq, and_true] exact SkolemAtoms.name_injective (Classical.choose_spec h.2).symm theorem Term.eval_witness (M : Structure P A) (v : Valuation M) (s : String) (U : List (Term A)) : Term.eval M v (witness s U) = M.skolem s (U.map (Term.eval M v)) := by rw [witness, Term.eval_node, skolemName_witness] /-! ## Changing one witness function -/ /-- `M` with the witness function of `s` replaced by `f`. -/ def Structure.withSkolem (M : Structure P A) (s : String) (f : List M.D → M.D) : Structure P A := { M with skolem := fun n => if n = s then f else M.skolem n } /-! ## Skolem names mentioned -/ /-- The Skolem names a term mentions. -/ def Term.names : Term A → List String | .var _ => [] | .atom _ => [] | .node cs => (match skolemName cs with | some (s, _) => [s] | none => []) ++ cs.attach.flatMap (fun c => Term.names c.val) termination_by t => sizeOf t decreasing_by have := List.sizeOf_lt_of_mem c.property simp_wf omega theorem Term.names_node (cs : List (Term A)) : Term.names (.node cs) = (match skolemName cs with | some (s, _) => [s] | none => []) ++ cs.flatMap Term.names := by rw [Term.names] simp theorem Term.names_node_mem (cs : List (Term A)) (c : Term A) (hc : c ∈ cs) (s : String) (hs : s ∈ c.names) : s ∈ Term.names (.node cs) := by rw [Term.names_node] apply List.mem_append_right rw [List.mem_flatMap] exact ⟨c, hc, hs⟩ theorem Term.names_node_skolem (cs : List (Term A)) (s : String) (args : List (Term A)) (h : skolemName cs = some (s, args)) : s ∈ Term.names (.node cs) := by rw [Term.names_node, h] simp /-- A term mentioning no changed name keeps its value. ```lean theorem Term.eval_withSkolem (M : Structure P A) (s : String) (f : List M.D → M.D) (v : Valuation M) : (t : Term A) → s ∉ t.names → Term.eval (M.withSkolem s f) v t = Term.eval M v t | .var x, _ => by rw [Term.eval_var, Term.eval_var] | .atom a, _ => by rw [Term.eval_atom, Term.eval_atom]; rfl | .node cs, hs => by rw [Term.eval_node, Term.eval_node] cases h : skolemName cs with | none => show M.tup _ = M.tup _ congr 1 apply List.map_congr_left intro c hc exact Term.eval_withSkolem M s f v c (fun hmem => hs (Term.names_node_mem cs c hc s hmem)) | some p => obtain ⟨s', args⟩ ``` #### `Formula.sat_withSkolem` The Skolem names a formula mentions. -/ def Formula.names : Formula P A → List String | .atom _ terms => terms.flatMap Term.names | .not f => f.names | .and parts => parts.attach.flatMap (fun f => Formula.names f.val) | .or parts => parts.attach.flatMap (fun f => Formula.names f.val) | .implies a c => a.names ++ c.names | .all _ body => body.names | .exists _ body => body.names termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega def Literal.names (l : Literal P A) : List String := l.terms.flatMap Term.names theorem Literal.sat_withSkolem (M : Structure P A) (s : String) (f : List M.D → M.D) (v : Valuation M) (l : Literal P A) (hs : s ∉ l.names) : Literal.sat (M.withSkolem s f) v l ↔ Literal.sat M v l := by have hterms : l.terms.map (Term.eval (M.withSkolem s f) v) = l.terms.map (Term.eval M v) := by apply List.map_congr_left intro t ht apply Term.eval_withSkolem intro hmem exact hs (List.mem_flatMap.mpr ⟨t, ht, hmem⟩) unfold Literal.sat show (if l.positive then M.pred l.pred _ else ¬ M.pred l.pred _) ↔ _ rw [hterms] theorem Formula.names_and_mem (parts : List (Formula P A)) (f : Formula P A) (hf : f ∈ parts) : ∀ s ∈ f.names, s ∈ Formula.names (.and parts) := by intro s hs rw [Formula.names] rw [List.mem_flatMap] exact ⟨⟨f, hf⟩, List.mem_attach _ _, hs⟩ theorem Formula.names_or_mem (parts : List (Formula P A)) (f : Formula P A) (hf : f ∈ parts) : ∀ s ∈ f.names, s ∈ Formula.names (.or parts) := by intro s hs rw [Formula.names] rw [List.mem_flatMap] exact ⟨⟨f, hf⟩, List.mem_attach _ _, hs⟩ /-- A formula mentioning no changed name keeps its truth. ```lean theorem Formula.sat_withSkolem (M : Structure P A) (s : String) (f : List M.D → M.D) : (φ : Formula P A) → (v : Valuation M) → s ∉ φ.names → (Formula.sat (M.withSkolem s f) v φ ↔ Formula.sat M v φ) | .atom p terms, v, hs => by rw [Formula.sat_atom, Formula.sat_atom] show M.pred p _ ↔ M.pred p _ have : terms.map (Term.eval (M.withSkolem s f) v) = terms.map (Term.eval M v) ``` #### `Term.eval_congr` The variables of a term. -/ def Term.vars : Term A → List String | .var x => [x] | .atom _ => [] | .node cs => cs.attach.flatMap (fun c => Term.vars c.val) termination_by t => sizeOf t decreasing_by have := List.sizeOf_lt_of_mem c.property simp_wf omega omit [SkolemAtoms A] in theorem Term.vars_node (cs : List (Term A)) : Term.vars (.node cs) = cs.flatMap Term.vars := by rw [Term.vars] simp /-- Two valuations agreeing on a term's variables give it the same value. ```lean theorem Term.eval_congr (M : Structure P A) (v v' : Valuation M) : (t : Term A) → (∀ x ∈ t.vars, v x = v' x) → Term.eval M v t = Term.eval M v' t | .var x, h => by rw [Term.eval_var, Term.eval_var] exact h x (by rw [Term.vars]; simp) | .atom a, _ => by rw [Term.eval_atom, Term.eval_atom] | .node cs, h => by rw [Term.eval_node, Term.eval_node] have hcs : ∀ c ∈ cs, Term.eval M v c = Term.eval M v' c ``` #### `Formula.sat_congr` The free variables of a formula. -/ def Formula.FV : Formula P A → List String | .atom _ terms => terms.flatMap Term.vars | .not f => f.FV | .and parts => parts.attach.flatMap (fun f => Formula.FV f.val) | .or parts => parts.attach.flatMap (fun f => Formula.FV f.val) | .implies a c => a.FV ++ c.FV | .all x body => body.FV.filter (· ≠ x) | .exists x body => body.FV.filter (· ≠ x) termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega omit [SkolemAtoms A] in theorem Formula.FV_and (parts : List (Formula P A)) : Formula.FV (.and parts) = parts.flatMap Formula.FV := by rw [Formula.FV] simp omit [SkolemAtoms A] in theorem Formula.FV_or (parts : List (Formula P A)) : Formula.FV (.or parts) = parts.flatMap Formula.FV := by rw [Formula.FV] simp omit [SkolemAtoms A] in theorem Valuation.update_congr {M : Structure P A} (v v' : Valuation M) (x : String) (d : M.D) (S : List String) (h : ∀ y ∈ S.filter (· ≠ x), v y = v' y) : ∀ y ∈ S, (v.update x d) y = (v'.update x d) y := by intro y hy unfold Valuation.update by_cases hyx : y = x · simp [hyx] · simp only [hyx, ↓reduceIte] exact h y (List.mem_filter.mpr ⟨hy, by simpa using hyx⟩) /-- Truth depends on a valuation only at the free variables. ```lean theorem Formula.sat_congr (M : Structure P A) : (φ : Formula P A) → (v v' : Valuation M) → (∀ x ∈ φ.FV, v x = v' x) → (Formula.sat M v φ ↔ Formula.sat M v' φ) | .atom p terms, v, v', h => by rw [Formula.sat_atom, Formula.sat_atom] have : terms.map (Term.eval M v) = terms.map (Term.eval M v') ``` #### `Formula.sat_subst` Substitution of free variables at the atoms, as the clause form applies it; binders are untouched, which is right when they avoid the substitution (`Formula.Avoids`). -/ def Formula.subst (σ : Subst A) : Formula P A → Formula P A | .atom p terms => .atom p (terms.map (Term.subst σ)) | .not f => .not (f.subst σ) | .and parts => .and (parts.attach.map (fun f => Formula.subst σ f.val)) | .or parts => .or (parts.attach.map (fun f => Formula.subst σ f.val)) | .implies a c => .implies (a.subst σ) (c.subst σ) | .all x body => .all x (body.subst σ) | .exists x body => .exists x (body.subst σ) termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega omit [SkolemAtoms A] in theorem Formula.subst_and (σ : Subst A) (parts : List (Formula P A)) : Formula.subst σ (.and parts) = .and (parts.map (Formula.subst σ)) := by rw [Formula.subst] simp omit [SkolemAtoms A] in theorem Formula.subst_or (σ : Subst A) (parts : List (Formula P A)) : Formula.subst σ (.or parts) = .or (parts.map (Formula.subst σ)) := by rw [Formula.subst] simp /-- The binders of a formula avoid a substitution: no bound variable is a key of it or a variable of one of its terms. -/ def Formula.Avoids (σ : Subst A) : Formula P A → Prop | .atom _ _ => True | .not f => f.Avoids σ | .and parts => ∀ f ∈ parts.attach, Formula.Avoids σ f.val | .or parts => ∀ f ∈ parts.attach, Formula.Avoids σ f.val | .implies a c => a.Avoids σ ∧ c.Avoids σ | .all x body => σ x = none ∧ (∀ y t, σ y = some t → x ∉ t.vars) ∧ body.Avoids σ | .exists x body => σ x = none ∧ (∀ y t, σ y = some t → x ∉ t.vars) ∧ body.Avoids σ termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega /-- Every term of a formula is well-formed. -/ def Formula.WF : Formula P A → Prop | .atom _ terms => ∀ t ∈ terms, Term.WF t | .not f => f.WF | .and parts => ∀ f ∈ parts.attach, Formula.WF f.val | .or parts => ∀ f ∈ parts.attach, Formula.WF f.val | .implies a c => a.WF ∧ c.WF | .all _ body => body.WF | .exists _ body => body.WF termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega theorem Valuation.ofSubst_update (M : Structure P A) (v : Valuation M) (σ : Subst A) (x : String) (d : M.D) (hx : σ x = none) (hvars : ∀ y t, σ y = some t → x ∉ t.vars) : Valuation.ofSubst M (v.update x d) σ = (Valuation.ofSubst M v σ).update x d := by funext y unfold Valuation.ofSubst Valuation.update by_cases hyx : y = x · subst hyx simp [hx] · simp only [hyx, ↓reduceIte] cases hσ : σ y with | none => simp | some t => simp only apply Term.eval_congr intro z hz have : z ≠ x := fun hzx => hvars y t hσ (hzx ▸ hz) simp [this] /-- The substitution lemma for formulas whose binders avoid the substitution. ```lean theorem Formula.sat_subst (M : Structure P A) (σ : Subst A) : (φ : Formula P A) → φ.WF → φ.Avoids σ → (v : Valuation M) → (Formula.sat M v (φ.subst σ) ↔ Formula.sat M (Valuation.ofSubst M v σ) φ) | .atom p terms, hwf, _, v => by rw [Formula.subst, Formula.sat_atom, Formula.sat_atom, List.map_map, Function.comp_def] rw [Term.evalList_subst M v σ terms (by rw [Formula.WF] at hwf; exact hwf)] | .not g, hwf, hav, v => by rw [Formula.subst, Formula.sat_not, Formula.sat_not] rw [Formula.WF] at hwf rw [Formula.Avoids] at hav rw [Formula.sat_subst M σ g hwf hav v] | .and parts, hwf, hav, v => by rw [Formula.subst_and, Formula.sat_and, Formula.sat_and] rw [Formula.WF] at hwf rw [Formula.Avoids] at hav constructor · intro h g hg have ``` ### `Sheaf/ClauseForm.lean` **The clause form, abstractly** `sheaf-kernel/src/clause_form.rs` turns a formula into clauses in three steps (`SHEAF/semantics.md` §5): negation normal form with Skolemization in one walk, then distribution into conjunctive normal form. This is that algorithm as a pure function on spec formulas, so that its soundness is a statement about logic alone; `SheafKernel.ClauseForm` shows the extracted kernel computes it. The walk carries a polarity (`neg`), the variables bound to witness terms so far (`env`), the universals in scope (`U`) and the Skolem name generator (`Sk`). A universal adds its variable to `U`; an existential binds its variable to the witness term over `U` and advances the generator. #### `Term.eval_withSkolems` A formula in negation normal form: literals under `and`/`or`. -/ inductive Nnf (P A : Type) where | lit (l : Literal P A) | and (parts : List (Nnf P A)) | or (parts : List (Nnf P A)) def Nnf.sat (M : Structure P A) : Valuation M → Nnf P A → Prop | v, .lit l => l.sat M v | v, .and parts => ∀ n ∈ parts.attach, Nnf.sat M v n.val | v, .or parts => ∃ n ∈ parts.attach, Nnf.sat M v n.val termination_by _ n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem n.property) all_goals omega theorem Nnf.sat_lit (M : Structure P A) (v : Valuation M) (l : Literal P A) : Nnf.sat M v (.lit l) ↔ l.sat M v := by rw [Nnf.sat] theorem Nnf.sat_and (M : Structure P A) (v : Valuation M) (parts : List (Nnf P A)) : Nnf.sat M v (.and parts) ↔ ∀ n ∈ parts, Nnf.sat M v n := by rw [Nnf.sat] constructor · intro h n hn exact h ⟨n, hn⟩ (List.mem_attach _ _) · intro h n _ exact h n.val n.property theorem Nnf.sat_or (M : Structure P A) (v : Valuation M) (parts : List (Nnf P A)) : Nnf.sat M v (.or parts) ↔ ∃ n ∈ parts, Nnf.sat M v n := by rw [Nnf.sat] constructor · rintro ⟨n, _, h⟩ exact ⟨n.val, n.property, h⟩ · rintro ⟨n, hn, h⟩ exact ⟨⟨n, hn⟩, List.mem_attach _ _, h⟩ /-- The Skolem names an `Nnf` mentions. -/ def Nnf.names : Nnf P A → List String | .lit l => l.names | .and parts => parts.attach.flatMap (fun n => Nnf.names n.val) | .or parts => parts.attach.flatMap (fun n => Nnf.names n.val) termination_by n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem n.property) all_goals omega theorem Nnf.names_and (parts : List (Nnf P A)) : Nnf.names (.and parts) = parts.flatMap Nnf.names := by rw [Nnf.names]; simp theorem Nnf.names_or (parts : List (Nnf P A)) : Nnf.names (.or parts) = parts.flatMap Nnf.names := by rw [Nnf.names]; simp /-! ## The generator and the environment -/ /-- The Skolem name generator: a namespace, the separator the names are written with, and a counter. The separator is a parameter so that nothing below depends on which string the kernel writes between namespace and counter. -/ structure Sk where ns : String sep : String counter : Nat /-- The name the generator issues next: ``. -/ def Sk.name (k : Sk) : String := k.ns ++ k.sep ++ toString k.counter def Sk.next (k : Sk) : Sk := ⟨k.ns, k.sep, k.counter + 1⟩ /-- The names `k` may still issue. -/ def Sk.Fresh (k : Sk) (s : String) : Prop := ∃ j, k.counter ≤ j ∧ s = k.ns ++ k.sep ++ toString j /-- Two generators of the same namespace and separator. -/ def Sk.Same (k k1 : Sk) : Prop := k1.ns = k.ns ∧ k1.sep = k.sep /-- Variables bound to witness terms, innermost first. -/ abbrev Env (A : Type) := List (String × Term A) def Env.find : Env A → String → Option (Term A) | [], _ => none | (y, t) :: rest, x => if x = y then some t else Env.find rest x def Env.subst (e : Env A) : Subst A := fun x => e.find x def Env.names (e : Env A) : List String := e.flatMap (fun p => p.2.names) def Env.keys (e : Env A) : List String := e.map Prod.fst /-! ## The walk -/ omit [SkolemAtoms A] in /-- A size that the rewriting of `implies` into `or [not a, c]` decreases. -/ def Formula.weight : Formula P A → Nat | .atom _ _ => 1 | .not f => f.weight + 1 | .and parts => (parts.attach.map (fun f => Formula.weight f.val)).sum + 1 | .or parts => (parts.attach.map (fun f => Formula.weight f.val)).sum + 1 | .implies a c => a.weight + c.weight + 4 | .all _ body => body.weight + 1 | .exists _ body => body.weight + 1 termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega omit [SkolemAtoms A] in theorem Formula.weight_and (parts : List (Formula P A)) : Formula.weight (.and parts) = (parts.map Formula.weight).sum + 1 := by rw [Formula.weight]; simp omit [SkolemAtoms A] in theorem Formula.weight_or (parts : List (Formula P A)) : Formula.weight (.or parts) = (parts.map Formula.weight).sum + 1 := by rw [Formula.weight]; simp omit [SkolemAtoms A] in theorem Formula.weight_pos (f : Formula P A) : 1 ≤ f.weight := by cases f <;> simp [Formula.weight, Formula.weight_and, Formula.weight_or] mutual /-- Negation normal form with Skolemization, as the kernel's `Skolemizer::nnf`. -/ def nnf (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) : Formula P A → Nnf P A × Sk | .atom p ts => (.lit ⟨!neg, p, ts.map (Term.subst env.subst)⟩, k) | .not f => nnf k (!neg) env U f | .and parts => let r := nnfList k neg env U parts (if neg then .or r.1 else .and r.1, r.2) | .or parts => let r := nnfList k neg env U parts (if neg then .and r.1 else .or r.1, r.2) | .implies a c => nnf k neg env U (.or [.not a, c]) | .all x body => if neg then nnf k.next neg ((x, witness k.name U) :: env) U body else nnf k neg env (U ++ [.var x]) body | .exists x body => if neg then nnf k neg env (U ++ [.var x]) body else nnf k.next neg ((x, witness k.name U) :: env) U body termination_by f => (f.weight, 0) decreasing_by all_goals simp_wf all_goals simp only [Formula.weight, Formula.weight_and, Formula.weight_or, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil] all_goals (apply Prod.Lex.left; omega) /-- The parts in order, threading the generator. -/ def nnfList (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) : List (Formula P A) → List (Nnf P A) × Sk | [] => ([], k) | f :: rest => let r := nnf k neg env U f let r' := nnfList r.2 neg env U rest (r.1 :: r'.1, r'.2) termination_by fs => ((fs.map Formula.weight).sum, 1) decreasing_by all_goals simp_wf · rcases Nat.eq_zero_or_pos (List.map Formula.weight rest).sum with h0 | hpos · rw [h0, Nat.add_zero] exact Prod.Lex.right _ (by decide) · exact Prod.Lex.left _ _ (by omega) · have := Formula.weight_pos f exact Prod.Lex.left _ _ (by omega) end /-! ## Changing witness functions -/ /-- `M` with the witness functions `fs` says, where it says one. -/ def Structure.withSkolems (M : Structure P A) (fs : String → Option (List M.D → M.D)) : Structure P A := { M with skolem := fun n => match fs n with | some f => f | none => M.skolem n } /-- Truth with the polarity the walk carries. -/ def pol (neg : Bool) (p : Prop) : Prop := if neg then ¬ p else p theorem Structure.withSkolems_skolem (M : Structure P A) (fs : String → Option (List M.D → M.D)) (n : String) : (M.withSkolems fs).skolem n = match fs n with | some f => f | none => M.skolem n := rfl /-- A term mentioning no changed name keeps its value. ```lean theorem Term.eval_withSkolems (M : Structure P A) (fs : String → Option (List M.D → M.D)) (v : Valuation M) : (t : Term A) → (∀ s ∈ t.names, fs s = none) → Term.eval (M.withSkolems fs) v t = Term.eval M v t | .var x, _ => by rw [Term.eval_var, Term.eval_var] | .atom a, _ => by rw [Term.eval_atom, Term.eval_atom]; rfl | .node cs, hs => by rw [Term.eval_node, Term.eval_node] cases h : skolemName cs with | none => show M.tup _ = M.tup _ congr 1 apply List.map_congr_left intro c hc exact Term.eval_withSkolems M fs v c (fun s hmem => hs s (Term.names_node_mem cs c hc s hmem)) | some p => obtain ⟨s', args⟩ ``` #### `Literal.sat_withSkolems` ```lean theorem Literal.sat_withSkolems (M : Structure P A) (fs : String → Option (List M.D → M.D)) (v : Valuation M) (l : Literal P A) (hs : ∀ s ∈ l.names, fs s = none) : Literal.sat (M.withSkolems fs) v l ↔ Literal.sat M v l ``` #### `Nnf.names_and_mem` ```lean theorem Nnf.names_and_mem (parts : List (Nnf P A)) (n : Nnf P A) (hn : n ∈ parts) : ∀ s ∈ n.names, s ∈ Nnf.names (.and parts) ``` #### `Nnf.names_or_mem` ```lean theorem Nnf.names_or_mem (parts : List (Nnf P A)) (n : Nnf P A) (hn : n ∈ parts) : ∀ s ∈ n.names, s ∈ Nnf.names (.or parts) ``` #### `Nnf.sat_withSkolems` An `Nnf` mentioning no changed name keeps its truth. ```lean theorem Nnf.sat_withSkolems (M : Structure P A) (fs : String → Option (List M.D → M.D)) : (n : Nnf P A) → (v : Valuation M) → (∀ s ∈ n.names, fs s = none) → (Nnf.sat (M.withSkolems fs) v n ↔ Nnf.sat M v n) | .lit l, v, hs => by rw [Nnf.sat_lit, Nnf.sat_lit] exact Literal.sat_withSkolems M fs v l (by rw [Nnf.names] at hs; exact hs) | .and parts, v, hs => by rw [Nnf.sat_and, Nnf.sat_and] constructor · intro h m hm exact (Nnf.sat_withSkolems M fs m v (fun s hsm => hs s (Nnf.names_and_mem parts m hm s hsm))).mp (h m hm) · intro h m hm exact (Nnf.sat_withSkolems M fs m v (fun s hsm => hs s (Nnf.names_and_mem parts m hm s hsm))).mpr (h m hm) | .or parts, v, hs => by rw [Nnf.sat_or, Nnf.sat_or] constructor · rintro ⟨m, hm, h⟩ exact ⟨m, hm, (Nnf.sat_withSkolems M fs m v (fun s hsm => hs s (Nnf.names_or_mem parts m hm s hsm))).mp h⟩ · rintro ⟨m, hm, h⟩ exact ⟨m, hm, (Nnf.sat_withSkolems M fs m v (fun s hsm => hs s (Nnf.names_or_mem parts m hm s hsm))).mpr h⟩ termination_by n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have ``` #### `Term.eval_withSkolems_congr` Two witness assignments agreeing on a term's names give it the same value. ```lean theorem Term.eval_withSkolems_congr (M : Structure P A) (fs fs' : String → Option (List M.D → M.D)) (v : Valuation M) : (t : Term A) → (∀ s ∈ t.names, fs s = fs' s) → Term.eval (M.withSkolems fs) v t = Term.eval (M.withSkolems fs') v t | .var x, _ => by rw [Term.eval_var, Term.eval_var] | .atom a, _ => by rw [Term.eval_atom, Term.eval_atom]; rfl | .node cs, hs => by rw [Term.eval_node, Term.eval_node] cases h : skolemName cs with | none => show M.tup _ = M.tup _ congr 1 apply List.map_congr_left intro c hc exact Term.eval_withSkolems_congr M fs fs' v c (fun s hmem => hs s (Term.names_node_mem cs c hc s hmem)) | some p => obtain ⟨s', args⟩ ``` #### `Literal.sat_withSkolems_congr` ```lean theorem Literal.sat_withSkolems_congr (M : Structure P A) (fs fs' : String → Option (List M.D → M.D)) (v : Valuation M) (l : Literal P A) (hs : ∀ s ∈ l.names, fs s = fs' s) : Literal.sat (M.withSkolems fs) v l ↔ Literal.sat (M.withSkolems fs') v l ``` #### `Nnf.sat_withSkolems_congr` Two witness assignments agreeing on an `Nnf`'s names give it the same truth. ```lean theorem Nnf.sat_withSkolems_congr (M : Structure P A) (fs fs' : String → Option (List M.D → M.D)) : (n : Nnf P A) → (v : Valuation M) → (∀ s ∈ n.names, fs s = fs' s) → (Nnf.sat (M.withSkolems fs) v n ↔ Nnf.sat (M.withSkolems fs') v n) | .lit l, v, hs => by rw [Nnf.sat_lit, Nnf.sat_lit] exact Literal.sat_withSkolems_congr M fs fs' v l (by rw [Nnf.names] at hs; exact hs) | .and parts, v, hs => by rw [Nnf.sat_and, Nnf.sat_and] constructor · intro h m hm exact (Nnf.sat_withSkolems_congr M fs fs' m v (fun s hsm => hs s (Nnf.names_and_mem parts m hm s hsm))).mp (h m hm) · intro h m hm exact (Nnf.sat_withSkolems_congr M fs fs' m v (fun s hsm => hs s (Nnf.names_and_mem parts m hm s hsm))).mpr (h m hm) | .or parts, v, hs => by rw [Nnf.sat_or, Nnf.sat_or] constructor · rintro ⟨m, hm, h⟩ exact ⟨m, hm, (Nnf.sat_withSkolems_congr M fs fs' m v (fun s hsm => hs s (Nnf.names_or_mem parts m hm s hsm))).mp h⟩ · rintro ⟨m, hm, h⟩ exact ⟨m, hm, (Nnf.sat_withSkolems_congr M fs fs' m v (fun s hsm => hs s (Nnf.names_or_mem parts m hm s hsm))).mpr h⟩ termination_by n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have ``` #### `Formula.sat_withSkolems` A formula mentioning no changed name keeps its truth. ```lean theorem Formula.sat_withSkolems (M : Structure P A) (fs : String → Option (List M.D → M.D)) : (φ : Formula P A) → (v : Valuation M) → (∀ s ∈ φ.names, fs s = none) → (Formula.sat (M.withSkolems fs) v φ ↔ Formula.sat M v φ) | .atom p terms, v, hs => by rw [Formula.sat_atom, Formula.sat_atom] show M.pred p _ ↔ M.pred p _ have : terms.map (Term.eval (M.withSkolems fs) v) = terms.map (Term.eval M v) ``` #### `Nat.digitChar_inj_of_lt_ten` ```lean theorem Nat.digitChar_inj_of_lt_ten {n m : Nat} (hn : n < 10) (hm : m < 10) (h : n.digitChar = m.digitChar) : n = m ``` #### `Nat.toDigits_ten_ne_nil` ```lean theorem Nat.toDigits_ten_ne_nil (n : Nat) : Nat.toDigits 10 n ≠ [] ``` #### `Nat.toDigits_ten_injective` ```lean theorem Nat.toDigits_ten_injective : ∀ (n m : Nat), Nat.toDigits 10 n = Nat.toDigits 10 m → n = m ``` #### `Nat.repr_injective_ten` ```lean theorem Nat.repr_injective_ten {n m : Nat} (h : toString n = toString m) : n = m ``` #### `Sk.name_eq_iff` ```lean theorem Sk.name_eq_iff (ns sep : String) (j j' : Nat) : ns ++ sep ++ toString j = ns ++ sep ++ toString j' ↔ j = j' ``` #### `Sk.same_refl` ```lean theorem Sk.same_refl (k : Sk) : Sk.Same k k ``` #### `Sk.same_next` ```lean theorem Sk.same_next (k : Sk) : Sk.Same k k.next ``` #### `Sk.Same.trans` ```lean theorem Sk.Same.trans {k k1 k2 : Sk} (h1 : Sk.Same k k1) (h2 : Sk.Same k1 k2) : Sk.Same k k2 ``` #### `Sk.fresh_next` ```lean theorem Sk.fresh_next {k : Sk} {s : String} (h : k.next.Fresh s) : k.Fresh s ``` #### `Sk.name_fresh` ```lean theorem Sk.name_fresh (k : Sk) : k.Fresh k.name ``` #### `Sk.name_not_fresh_next` ```lean theorem Sk.name_not_fresh_next (k : Sk) : ¬ k.next.Fresh k.name ``` #### `Sk.not_fresh_of_lt` ```lean theorem Sk.not_fresh_of_lt {k k1 : Sk} (hs : Sk.Same k k1) (hle : k.counter ≤ k1.counter) {s : String} (h : ¬ k.Fresh s) : ¬ k1.Fresh s ``` #### `Formula.Scoped.avoids` The binders of a formula avoid `bound` and each other: a binder is not in `bound`, and its body is scoped under `bound` with it. -/ def Formula.Scoped (bound : String → Prop) : Formula P A → Prop | .atom _ _ => True | .not f => f.Scoped bound | .and parts => ∀ f ∈ parts.attach, Formula.Scoped bound f.val | .or parts => ∀ f ∈ parts.attach, Formula.Scoped bound f.val | .implies a c => a.Scoped bound ∧ c.Scoped bound | .all x body => ¬ bound x ∧ body.Scoped (fun y => y = x ∨ bound y) | .exists x body => ¬ bound x ∧ body.Scoped (fun y => y = x ∨ bound y) termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega theorem Formula.Scoped.mono {b1 b2 : String → Prop} (h : ∀ y, b1 y → b2 y) : (φ : Formula P A) → φ.Scoped b2 → φ.Scoped b1 | .atom _ _, _ => by rw [Formula.Scoped]; trivial | .not f, hs => by rw [Formula.Scoped] at hs ⊢ exact Formula.Scoped.mono h f hs | .and parts, hs => by rw [Formula.Scoped] at hs ⊢ intro f hf exact Formula.Scoped.mono h f.val (hs f hf) | .or parts, hs => by rw [Formula.Scoped] at hs ⊢ intro f hf exact Formula.Scoped.mono h f.val (hs f hf) | .implies a c, hs => by rw [Formula.Scoped] at hs ⊢ exact ⟨Formula.Scoped.mono h a hs.1, Formula.Scoped.mono h c hs.2⟩ | .all x body, hs => by rw [Formula.Scoped] at hs ⊢ refine ⟨fun hb => hs.1 (h x hb), ?_⟩ exact Formula.Scoped.mono (fun y hy => hy.elim Or.inl (fun hb => Or.inr (h y hb))) body hs.2 | .exists x body, hs => by rw [Formula.Scoped] at hs ⊢ refine ⟨fun hb => hs.1 (h x hb), ?_⟩ exact Formula.Scoped.mono (fun y hy => hy.elim Or.inl (fun hb => Or.inr (h y hb))) body hs.2 termination_by φ => sizeOf φ decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem f.property) all_goals omega /-- A scoped formula's binders avoid a substitution whose keys and whose terms' variables are all bound. ```lean theorem Formula.Scoped.avoids (σ : Subst A) (bound : String → Prop) (hkeys : ∀ y t, σ y = some t → bound y) (hvars : ∀ y t, σ y = some t → ∀ z ∈ t.vars, bound z) : (φ : Formula P A) → φ.Scoped bound → φ.Avoids σ | .atom _ _, _ => by rw [Formula.Avoids]; trivial | .not f, hs => by rw [Formula.Scoped] at hs rw [Formula.Avoids] exact Formula.Scoped.avoids σ bound hkeys hvars f hs | .and parts, hs => by rw [Formula.Scoped] at hs rw [Formula.Avoids] intro f hf exact Formula.Scoped.avoids σ bound hkeys hvars f.val (hs f hf) | .or parts, hs => by rw [Formula.Scoped] at hs rw [Formula.Avoids] intro f hf exact Formula.Scoped.avoids σ bound hkeys hvars f.val (hs f hf) | .implies a c, hs => by rw [Formula.Scoped] at hs rw [Formula.Avoids] exact ⟨Formula.Scoped.avoids σ bound hkeys hvars a hs.1, Formula.Scoped.avoids σ bound hkeys hvars c hs.2⟩ | .all x body, hs => by rw [Formula.Scoped] at hs rw [Formula.Avoids] refine ⟨?_, ?_, ?_⟩ · cases hσ : σ x with | none => rfl | some t => exact absurd (hkeys x t hσ) hs.1 · intro y t hyt hx exact hs.1 (hvars y t hyt x hx) · exact Formula.Scoped.avoids σ _ (fun y t h => Or.inr (hkeys y t h)) (fun y t h z hz => Or.inr (hvars y t h z hz)) body hs.2 | .exists x body, hs => by rw [Formula.Scoped] at hs rw [Formula.Avoids] refine ⟨?_, ?_, ?_⟩ · cases hσ : σ x with | none => rfl | some t => exact absurd (hkeys x t hσ) hs.1 · intro y t hyt hx exact hs.1 (hvars y t hyt x hx) · exact Formula.Scoped.avoids σ _ (fun y t h => Or.inr (hkeys y t h)) (fun y t h z hz => Or.inr (hvars y t h z hz)) body hs.2 termination_by φ => sizeOf φ decreasing_by all_goals simp_wf all_goals try (have ``` #### `Term.vars_subst_subset` ```lean theorem Term.vars_subst_subset (σ : Subst A) : (t : Term A) → ∀ z ∈ (t.subst σ).vars, (z ∈ t.vars ∧ σ z = none) ∨ ∃ y u, σ y = some u ∧ z ∈ u.vars | .var x, z, hz => by unfold Term.subst at hz cases hσ : σ x with | none => rw [hσ] at hz rw [Term.vars] at hz simp at hz subst hz exact Or.inl ⟨by rw [Term.vars]; simp, hσ⟩ | some u => rw [hσ] at hz exact Or.inr ⟨x, u, hσ, hz⟩ | .atom _, z, hz => by rw [Term.subst, Term.vars] at hz; simp at hz | .node cs, z, hz => by rw [Term.subst, Term.vars_node, List.mem_flatMap] at hz obtain ⟨c', hc', hz⟩ ``` #### `Term.names_subst_subset` ```lean theorem Term.names_subst_subset (σ : Subst A) : (t : Term A) → t.WF → ∀ s ∈ (t.subst σ).names, s ∈ t.names ∨ ∃ y u, σ y = some u ∧ s ∈ u.names | .var x, _, s, hs => by unfold Term.subst at hs cases hσ : σ x with | none => rw [hσ] at hs; rw [Term.names] at hs; simp at hs | some u => rw [hσ] at hs; exact Or.inr ⟨x, u, hσ, hs⟩ | .atom _, _, s, hs => by rw [Term.subst, Term.names] at hs; simp at hs | .node cs, hwf, s, hs => by rw [Term.subst, Term.names_node, skolemName_subst σ cs hwf] at hs rcases List.mem_append.mp hs with hs | hs · left rw [Term.names_node] apply List.mem_append_left cases h : skolemName cs with | none => rw [h] at hs; simp at hs | some p => rw [h] at hs; simpa using hs · rw [List.mem_flatMap] at hs obtain ⟨c', hc', hs⟩ ``` ### `Sheaf/Skolemization.lean` **Soundness of negation normal form with Skolemization** `nnf` (`Sheaf.ClauseForm`) is sound: when a formula holds (with the walk's polarity) in a structure, some choice of witness functions for the names the walk issues makes its output hold, uniformly over valuations. The witness for an existential at universals `U` is a function of the values of `U`, chosen for a valuation with those values; the body's truth depends only on those values and the bound variable, so the choice serves every valuation with them. #### `pol_not` ```lean theorem pol_not (neg : Bool) (p : Prop) : pol neg (¬ p) ↔ pol (!neg) p ``` #### `pol_iff` ```lean theorem pol_iff (neg : Bool) {p q : Prop} (h : p ↔ q) : pol neg p ↔ pol neg q ``` #### `Valuation.update_self` ```lean theorem Valuation.update_self {M : Structure P A} (v : Valuation M) (x : String) : v.update x (v x) = v ``` #### `Env.find_cons` ```lean theorem Env.find_cons (x : String) (t : Term A) (e : Env A) (y : String) : Env.find ((x, t) :: e) y = if y = x then some t else e.find y ``` #### `Env.find_mem` ```lean theorem Env.find_mem (e : Env A) (y : String) (u : Term A) (h : e.find y = some u) : (y, u) ∈ e ``` #### `witness_vars` ```lean theorem witness_vars (s : String) (U : List (Term A)) : (witness s U).vars = U.flatMap Term.vars ``` #### `witness_names` ```lean theorem witness_names (s : String) (U : List (Term A)) : ∀ s' ∈ (witness s U).names, s' = s ∨ s' ∈ (Term.node U).names ``` #### `names_node_vars` A tuple of variables mentions no Skolem name. ```lean theorem names_node_vars (U : List (Term A)) (hU : ∀ u ∈ U, u.isVar) : (Term.node U).names = [] ``` #### `var_mem_of_vars` The variables of a variable list are its variables. ```lean theorem var_mem_of_vars (U : List (Term A)) (hU : ∀ u ∈ U, u.isVar) (y : String) (hy : y ∈ U.flatMap Term.vars) : Term.var y ∈ U ``` #### `Formula.FV_subst_subset` Free variables of a substituted formula. ```lean theorem Formula.FV_subst_subset (σ : Subst A) : (φ : Formula P A) → ∀ z ∈ (φ.subst σ).FV, (z ∈ φ.FV ∧ σ z = none) ∨ ∃ y u, σ y = some u ∧ z ∈ u.vars | .atom p terms, z, hz => by rw [Formula.subst, Formula.FV, List.mem_flatMap] at hz obtain ⟨t', ht', hz⟩ ``` #### `Formula.names_subst_subset` Skolem names of a substituted formula. ```lean theorem Formula.names_subst_subset (σ : Subst A) : (φ : Formula P A) → φ.WF → ∀ s ∈ (φ.subst σ).names, s ∈ φ.names ∨ ∃ y u, σ y = some u ∧ s ∈ u.names | .atom p terms, hwf, s, hs => by rw [Formula.subst, Formula.names, List.mem_flatMap] at hs obtain ⟨t', ht', hs⟩ ``` #### `nnf_atom` ```lean theorem nnf_atom (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (p : P) (ts : List (Term A)) : nnf k neg env U (.atom p ts) = (.lit ⟨!neg, p, ts.map (Term.subst env.subst)⟩, k) ``` #### `nnf_not` ```lean theorem nnf_not (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (f : Formula P A) : nnf k neg env U (.not f) = nnf k (!neg) env U f ``` #### `nnf_and` ```lean theorem nnf_and (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (parts : List (Formula P A)) : nnf k neg env U (.and parts) = (if neg then .or (nnfList k neg env U parts).1 else .and (nnfList k neg env U parts).1, (nnfList k neg env U parts).2) ``` #### `nnf_or` ```lean theorem nnf_or (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (parts : List (Formula P A)) : nnf k neg env U (.or parts) = (if neg then .and (nnfList k neg env U parts).1 else .or (nnfList k neg env U parts).1, (nnfList k neg env U parts).2) ``` #### `nnf_implies` ```lean theorem nnf_implies (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (a c : Formula P A) : nnf k neg env U (.implies a c) = nnf k neg env U (.or [.not a, c]) ``` #### `nnf_all` ```lean theorem nnf_all (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (x : String) (body : Formula P A) : nnf k neg env U (.all x body) = if neg then nnf k.next neg ((x, witness k.name U) :: env) U body else nnf k neg env (U ++ [.var x]) body ``` #### `nnf_exists` ```lean theorem nnf_exists (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (x : String) (body : Formula P A) : nnf k neg env U (.exists x body) = if neg then nnf k neg env (U ++ [.var x]) body else nnf k.next neg ((x, witness k.name U) :: env) U body ``` #### `nnfList_nil` ```lean theorem nnfList_nil (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) : nnfList k neg env U ([] : List (Formula P A)) = ([], k) ``` #### `nnfList_cons` ```lean theorem nnfList_cons (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (f : Formula P A) (rest : List (Formula P A)) : nnfList k neg env U (f :: rest) = ((nnf k neg env U f).1 :: (nnfList (nnf k neg env U f).2 neg env U rest).1, (nnfList (nnf k neg env U f).2 neg env U rest).2) ``` #### `Inv.advance` The invariants the walk keeps: the formula is well-formed; the universals are variables; binders avoid the bound variables (the environment's keys and the universals) and each other; the environment's terms range over the universals; the free variables are bound; and no name the generator may still issue is in use. -/ structure Inv (k : Sk) (env : Env A) (U : List (Term A)) (φ : Formula P A) : Prop where wf : φ.WF uvars : ∀ u ∈ U, u.isVar binders : φ.Scoped (fun y => y ∈ env.keys ∨ y ∈ U.flatMap Term.vars) envVars : ∀ p ∈ env, ∀ z ∈ p.2.vars, z ∈ U.flatMap Term.vars fv : ∀ z ∈ φ.FV, z ∈ env.keys ∨ z ∈ U.flatMap Term.vars freshφ : ∀ s ∈ φ.names, ¬ k.Fresh s freshEnv : ∀ s ∈ env.names, ¬ k.Fresh s omit [SkolemAtoms A] in theorem Sk.fresh_of_le {k k1 : Sk} (hs : Sk.Same k k1) (hle : k.counter ≤ k1.counter) {s : String} (h : k1.Fresh s) : k.Fresh s := by obtain ⟨j, hj, rfl⟩ := h exact ⟨j, by omega, by rw [hs.1, hs.2]⟩ /-- Advancing the generator keeps the invariants. ```lean theorem Inv.advance {k k1 : Sk} {env : Env A} {U : List (Term A)} {φ : Formula P A} (h : Inv k env U φ) (hs : Sk.Same k k1) (hle : k.counter ≤ k1.counter) : Inv k1 env U φ ``` #### `Inv.not` ```lean theorem Inv.not {k : Sk} {env : Env A} {U : List (Term A)} {f : Formula P A} (h : Inv k env U (.not f)) : Inv k env U f ``` #### `Inv.and_part` ```lean theorem Inv.and_part {k : Sk} {env : Env A} {U : List (Term A)} {parts : List (Formula P A)} (h : Inv k env U (.and parts)) (f : Formula P A) (hf : f ∈ parts) : Inv k env U f ``` #### `Inv.or_part` ```lean theorem Inv.or_part {k : Sk} {env : Env A} {U : List (Term A)} {parts : List (Formula P A)} (h : Inv k env U (.or parts)) (f : Formula P A) (hf : f ∈ parts) : Inv k env U f ``` #### `Formula.names_implies_or` ```lean theorem Formula.names_implies_or (a c : Formula P A) : ∀ s, s ∈ Formula.names (.or [.not a, c]) ↔ s ∈ Formula.names (.implies a c) ``` #### `Inv.implies_or` ```lean theorem Inv.implies_or {k : Sk} {env : Env A} {U : List (Term A)} {a c : Formula P A} (h : Inv k env U (.implies a c)) : Inv k env U (.or [.not a, c]) ``` #### `Formula.sat_implies_or` ```lean theorem Formula.sat_implies_or (M : Structure P A) (v : Valuation M) (σ : Subst A) (a c : Formula P A) : Formula.sat M v ((Formula.implies a c).subst σ) ↔ Formula.sat M v ((Formula.or [.not a, c]).subst σ) ``` #### `Term.eval_withSkolems_twice` `fs` sets witness functions only for names issued between `k` and `k'`. -/ def FreshRange (k k' : Sk) {M : Structure P A} (fs : String → Option (List M.D → M.D)) : Prop := ∀ s, fs s ≠ none → k.Fresh s ∧ ¬ k'.Fresh s /-- What the walk guarantees for one formula: the generator only advances; the output's names are the input's, the environment's, or freshly issued; and in any structure, some witness functions for the fresh names make the output hold wherever the input holds (with the polarity), uniformly over valuations. -/ def Sound (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (φ : Formula P A) (n : Nnf P A) (k' : Sk) : Prop := Sk.Same k k' ∧ k.counter ≤ k'.counter ∧ (∀ s ∈ n.names, s ∈ φ.names ∨ s ∈ env.names ∨ (k.Fresh s ∧ ¬ k'.Fresh s)) ∧ ∀ M : Structure P A, ∃ fs : String → Option (List M.D → M.D), FreshRange k k' fs ∧ ∀ v : Valuation M, pol neg (Formula.sat M v (φ.subst env.subst)) → Nnf.sat (M.withSkolems fs) v n /-- The same for a list of parts, pointwise with one choice of witness functions. -/ def SoundList (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (parts : List (Formula P A)) (ns : List (Nnf P A)) (k' : Sk) : Prop := Sk.Same k k' ∧ k.counter ≤ k'.counter ∧ ns.length = parts.length ∧ (∀ s ∈ ns.flatMap Nnf.names, (∃ f ∈ parts, s ∈ f.names) ∨ s ∈ env.names ∨ (k.Fresh s ∧ ¬ k'.Fresh s)) ∧ ∀ M : Structure P A, ∃ fs : String → Option (List M.D → M.D), FreshRange k k' fs ∧ ∀ v : Valuation M, ∀ (i : Nat) (hi : i < parts.length) (hi' : i < ns.length), pol neg (Formula.sat M v (parts[i].subst env.subst)) → Nnf.sat (M.withSkolems fs) v ns[i] /-! ## Two rounds of witness assignments -/ /-- Setting witness functions twice is setting the merge once. ```lean theorem Term.eval_withSkolems_twice (M : Structure P A) (g : String → Option (List M.D → M.D)) (fs : String → Option (List (M.withSkolems g).D → (M.withSkolems g).D)) (v : Valuation M) : (t : Term A) → Term.eval ((M.withSkolems g).withSkolems fs) v t = Term.eval (M.withSkolems (fun s => match fs s with | some f => some f | none => g s)) v t | .var x => by rw [Term.eval_var, Term.eval_var] | .atom a => by rw [Term.eval_atom, Term.eval_atom]; rfl | .node cs => by rw [Term.eval_node, Term.eval_node] cases h : skolemName cs with | none => dsimp only show M.tup _ = M.tup _ congr 1 apply List.map_congr_left intro c hc exact Term.eval_withSkolems_twice M g fs v c | some p => obtain ⟨s', args⟩ ``` #### `Literal.sat_withSkolems_twice` ```lean theorem Literal.sat_withSkolems_twice (M : Structure P A) (g : String → Option (List M.D → M.D)) (fs : String → Option (List (M.withSkolems g).D → (M.withSkolems g).D)) (v : Valuation M) (l : Literal P A) : Literal.sat ((M.withSkolems g).withSkolems fs) v l ↔ Literal.sat (M.withSkolems (fun s => match fs s with | some f => some f | none => g s)) v l ``` #### `Nnf.sat_withSkolems_twice` ```lean theorem Nnf.sat_withSkolems_twice (M : Structure P A) (g : String → Option (List M.D → M.D)) (fs : String → Option (List (M.withSkolems g).D → (M.withSkolems g).D)) : (n : Nnf P A) → (v : Valuation M) → (Nnf.sat ((M.withSkolems g).withSkolems fs) v n ↔ Nnf.sat (M.withSkolems (fun s => match fs s with | some f => some f | none => g s)) v n) | .lit l, v => by rw [Nnf.sat_lit, Nnf.sat_lit] exact Literal.sat_withSkolems_twice M g fs v l | .and parts, v => by rw [Nnf.sat_and, Nnf.sat_and] constructor · intro h m hm exact (Nnf.sat_withSkolems_twice M g fs m v).mp (h m hm) · intro h m hm exact (Nnf.sat_withSkolems_twice M g fs m v).mpr (h m hm) | .or parts, v => by rw [Nnf.sat_or, Nnf.sat_or] constructor · rintro ⟨m, hm, h⟩ exact ⟨m, hm, (Nnf.sat_withSkolems_twice M g fs m v).mp h⟩ · rintro ⟨m, hm, h⟩ exact ⟨m, hm, (Nnf.sat_withSkolems_twice M g fs m v).mpr h⟩ termination_by n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have ``` #### `Env.find_none_of_not_mem_keys` ```lean theorem Env.find_none_of_not_mem_keys (e : Env A) (x : String) (h : x ∉ e.keys) : e.find x = none ``` #### `Env.find_some_of_mem_keys` ```lean theorem Env.find_some_of_mem_keys (e : Env A) (x : String) (h : x ∈ e.keys) : ∃ u, e.find x = some u ``` #### `Env.mem_keys_of_find_some` ```lean theorem Env.mem_keys_of_find_some (e : Env A) (y : String) (u : Term A) (h : e.find y = some u) : y ∈ e.keys ``` #### `Env.names_cons` ```lean theorem Env.names_cons (x : String) (t : Term A) (e : Env A) : Env.names ((x, t) :: e) = t.names ++ e.names ``` #### `Env.keys_cons` ```lean theorem Env.keys_cons (x : String) (t : Term A) (e : Env A) : Env.keys ((x, t) :: e) = x :: e.keys ``` #### `eval_vars_withSkolems` Evaluation of a list of variables is the same in any two structures on the same domain with the same tupling and atoms — here, after a change of witness functions. ```lean theorem eval_vars_withSkolems (M : Structure P A) (fs : String → Option (List M.D → M.D)) (v : Valuation M) (U : List (Term A)) (hU : ∀ u ∈ U, u.isVar) : U.map (Term.eval (M.withSkolems fs) v) = U.map (Term.eval M v) ``` #### `Inv.universal` The invariants for the body of a universal binder. ```lean theorem Inv.universal {k : Sk} {env : Env A} {U : List (Term A)} {x : String} {body : Formula P A} (hwf : body.WF) (huvars : ∀ u ∈ U, u.isVar) (hsc : body.Scoped (fun y => y = x ∨ (y ∈ env.keys ∨ y ∈ U.flatMap Term.vars))) (henv : ∀ p ∈ env, ∀ z ∈ p.2.vars, z ∈ U.flatMap Term.vars) (hfv : ∀ z ∈ body.FV.filter (· ≠ x), z ∈ env.keys ∨ z ∈ U.flatMap Term.vars) (hfresh : ∀ s ∈ body.names, ¬ k.Fresh s) (hfreshEnv : ∀ s ∈ env.names, ¬ k.Fresh s) : Inv k env (U ++ [.var x]) body ``` #### `Inv.skolem` The invariants for the body of a Skolemized binder. ```lean theorem Inv.skolem {k : Sk} {env : Env A} {U : List (Term A)} {x : String} {body : Formula P A} (hwf : body.WF) (huvars : ∀ u ∈ U, u.isVar) (hsc : body.Scoped (fun y => y = x ∨ (y ∈ env.keys ∨ y ∈ U.flatMap Term.vars))) (henv : ∀ p ∈ env, ∀ z ∈ p.2.vars, z ∈ U.flatMap Term.vars) (hfv : ∀ z ∈ body.FV.filter (· ≠ x), z ∈ env.keys ∨ z ∈ U.flatMap Term.vars) (hfresh : ∀ s ∈ body.names, ¬ k.Fresh s) (hfreshEnv : ∀ s ∈ env.names, ¬ k.Fresh s) : Inv k.next ((x, witness k.name U) :: env) U body ``` #### `universal_sound` The universal reading of a binder: the body's result serves. ```lean theorem universal_sound (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (x : String) (body : Formula P A) (n : Nnf P A) (k' : Sk) (hs : Sound k neg env (U ++ [.var x]) body n k') (B : Formula P A) (hnames : ∀ s, s ∈ B.names ↔ s ∈ body.names) (hsem : ∀ (M : Structure P A) (v : Valuation M), pol neg (Formula.sat M v (B.subst env.subst)) → pol neg (Formula.sat M v (body.subst env.subst))) : Sound k neg env U B n k' ``` #### `skolem_sound` The Skolemized reading of a binder: a witness function for the fresh name, chosen from the values of the universals, serves every valuation. ```lean theorem skolem_sound (k : Sk) (neg : Bool) (env : Env A) (U : List (Term A)) (x : String) (body : Formula P A) (n : Nnf P A) (k' : Sk) (hwf : body.WF) (huvars : ∀ u ∈ U, u.isVar) (hsc : body.Scoped (fun y => y = x ∨ (y ∈ env.keys ∨ y ∈ U.flatMap Term.vars))) (hxB : ¬ (x ∈ env.keys ∨ x ∈ U.flatMap Term.vars)) (henv : ∀ p ∈ env, ∀ z ∈ p.2.vars, z ∈ U.flatMap Term.vars) (hfv : ∀ z ∈ body.FV.filter (· ≠ x), z ∈ env.keys ∨ z ∈ U.flatMap Term.vars) (hfresh : ∀ s ∈ body.names, ¬ k.Fresh s) (hfreshEnv : ∀ s ∈ env.names, ¬ k.Fresh s) (hs : Sound k.next neg ((x, witness k.name U) :: env) U body n k') (B : Formula P A) (hnames : ∀ s, s ∈ B.names ↔ s ∈ body.names) (hsem : ∀ (M : Structure P A) (v : Valuation M), pol neg (Formula.sat M v (B.subst env.subst)) → ∃ d : M.D, pol neg (Formula.sat M (v.update x d) (body.subst env.subst))) : Sound k neg env U B n k' ``` ### `Sheaf/Cnf.lean` **Distribution into clauses, and the clause form's soundness** The last step of the clause form distributes `or` over `and` (`sheaf-kernel/src/clause_form.rs: cnf`, without the capacity bound, which only refuses). A negation normal form holds under a valuation exactly when every clause of its distribution does. With `nnf_sound`, this gives the clause form's soundness: wherever a closed, scoped, well-formed formula is true, some witness functions for the issued Skolem names make all of its clauses true. #### `cnf_sound` Every union of a clause of `partials` with a clause of `group`. -/ def distribute (partials group : List (Clause P A)) : List (Clause P A) := partials.flatMap (fun p => group.map (fun c => p ++ c)) /-- Conjunctive normal form by distribution. -/ def cnf : Nnf P A → List (Clause P A) | .lit l => [[l]] | .and parts => (parts.attach.map (fun n => cnf n.val)).flatten | .or parts => (parts.attach.map (fun n => cnf n.val)).foldl distribute [[]] termination_by n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem n.property) all_goals omega omit [SkolemAtoms A] in theorem cnf_and (parts : List (Nnf P A)) : cnf (.and parts) = (parts.map cnf).flatten := by rw [cnf]; simp omit [SkolemAtoms A] in theorem cnf_or (parts : List (Nnf P A)) : cnf (.or parts) = (parts.map cnf).foldl distribute [[]] := by rw [cnf]; simp /-- All clauses of a list hold under `v`. -/ def satAll (M : Structure P A) (v : Valuation M) (cs : List (Clause P A)) : Prop := ∀ c ∈ cs, c.satAt M v theorem satAll_distribute (M : Structure P A) (v : Valuation M) (ps g : List (Clause P A)) : satAll M v (distribute ps g) ↔ satAll M v ps ∨ satAll M v g := by classical unfold satAll distribute constructor · intro h by_cases hps : ∀ p ∈ ps, p.satAt M v · exact Or.inl hps · right rw [not_forall] at hps obtain ⟨p, hp⟩ := hps rw [Classical.not_imp] at hp obtain ⟨hp, hpf⟩ := hp intro c hc have := h (p ++ c) (List.mem_flatMap.mpr ⟨p, hp, List.mem_map.mpr ⟨c, hc, rfl⟩⟩) obtain ⟨l, hl, hsat⟩ := this rcases List.mem_append.mp hl with hl | hl · exact absurd ⟨l, hl, hsat⟩ hpf · exact ⟨l, hl, hsat⟩ · intro h x hx rw [List.mem_flatMap] at hx obtain ⟨p, hp, hx⟩ := hx obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hx rcases h with h | h · obtain ⟨l, hl, hsat⟩ := h p hp exact ⟨l, List.mem_append_left _ hl, hsat⟩ · obtain ⟨l, hl, hsat⟩ := h c hc exact ⟨l, List.mem_append_right _ hl, hsat⟩ theorem satAll_foldl_distribute (M : Structure P A) (v : Valuation M) : ∀ (gs : List (List (Clause P A))) (acc : List (Clause P A)), satAll M v (gs.foldl distribute acc) ↔ satAll M v acc ∨ ∃ g ∈ gs, satAll M v g := by intro gs induction gs with | nil => intro acc simp [List.foldl] | cons g rest ih => intro acc rw [List.foldl_cons, ih, satAll_distribute] constructor · rintro ((h | h) | ⟨g', hg', h⟩) · exact Or.inl h · exact Or.inr ⟨g, List.mem_cons_self, h⟩ · exact Or.inr ⟨g', List.mem_cons_of_mem _ hg', h⟩ · rintro (h | ⟨g', hg', h⟩) · exact Or.inl (Or.inl h) · rcases List.mem_cons.mp hg' with rfl | hg' · exact Or.inl (Or.inr h) · exact Or.inr ⟨g', hg', h⟩ theorem satAll_empty_clause (M : Structure P A) (v : Valuation M) : ¬ satAll M v [[]] := by intro h obtain ⟨l, hl, _⟩ := h [] List.mem_cons_self simp at hl /-- A negation normal form holds exactly when all clauses of its distribution do. ```lean theorem cnf_sound (M : Structure P A) (v : Valuation M) : (n : Nnf P A) → (Nnf.sat M v n ↔ satAll M v (cnf n)) | .lit l => by rw [Nnf.sat_lit, cnf] unfold satAll Clause.satAt simp | .and parts => by rw [Nnf.sat_and, cnf_and] unfold satAll constructor · intro h c hc rw [List.mem_flatten] at hc obtain ⟨g, hg, hc⟩ ``` #### `Nnf.names_of_lit` The literals of a negation normal form, in order. -/ def Nnf.lits : Nnf P A → List (Literal P A) | .lit l => [l] | .and parts => (parts.attach.map (fun n => Nnf.lits n.val)).flatten | .or parts => (parts.attach.map (fun n => Nnf.lits n.val)).flatten termination_by n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have := List.sizeOf_lt_of_mem n.property) all_goals omega omit [SkolemAtoms A] in theorem Nnf.lits_and (parts : List (Nnf P A)) : Nnf.lits (.and parts) = (parts.map Nnf.lits).flatten := by rw [Nnf.lits]; simp omit [SkolemAtoms A] in theorem Nnf.lits_or (parts : List (Nnf P A)) : Nnf.lits (.or parts) = (parts.map Nnf.lits).flatten := by rw [Nnf.lits]; simp /-- A literal's names are among the normal form's. ```lean theorem Nnf.names_of_lit : (n : Nnf P A) → ∀ l ∈ n.lits, ∀ s ∈ l.names, s ∈ n.names | .lit l' => by rw [Nnf.lits, Nnf.names] intro l hl s hs rw [List.mem_singleton] at hl subst hl exact hs | .and parts => by rw [Nnf.lits_and] intro l hl s hs rw [List.mem_flatten] at hl obtain ⟨ls, hls, hl⟩ ``` #### `distribute_lits` ```lean theorem distribute_lits (Q : Literal P A → Prop) (ps g : List (Clause P A)) (hp : ∀ c ∈ ps, ∀ l ∈ c, Q l) (hg : ∀ c ∈ g, ∀ l ∈ c, Q l) : ∀ c ∈ distribute ps g, ∀ l ∈ c, Q l ``` #### `foldl_distribute_lits` ```lean theorem foldl_distribute_lits (Q : Literal P A → Prop) : ∀ (gs : List (List (Clause P A))) (acc : List (Clause P A)), (∀ c ∈ acc, ∀ l ∈ c, Q l) → (∀ g ∈ gs, ∀ c ∈ g, ∀ l ∈ c, Q l) → ∀ c ∈ gs.foldl distribute acc, ∀ l ∈ c, Q l ``` #### `cnf_lits` Every literal of a clause of the distribution is a literal of the normal form. ```lean theorem cnf_lits : (n : Nnf P A) → ∀ c ∈ cnf n, ∀ l ∈ c, l ∈ n.lits | .lit l' => by rw [cnf, Nnf.lits] intro c hc l hl rw [List.mem_singleton] at hc subst hc exact hl | .and parts => by rw [cnf_and, Nnf.lits_and] intro c hc l hl rw [List.mem_flatten] at hc obtain ⟨g, hg, hc⟩ ``` #### `Clause.true_withSkolems_congr` The Skolem names a clause mentions. -/ def Clause.names (c : Clause P A) : List String := c.flatMap Literal.names /-- A clause's truth depends on the witness functions only at its names. ```lean theorem Clause.true_withSkolems_congr (M : Structure P A) (fs fs' : String → Option (List M.D → M.D)) (c : Clause P A) (hs : ∀ s ∈ c.names, fs s = fs' s) (h : Clause.true (M.withSkolems fs) c) : Clause.true (M.withSkolems fs') c ``` #### `Term.subst_none` ```lean theorem Term.subst_none : (t : Term A) → t.subst (fun _ => none) = t | .var x => by rw [Term.subst] | .atom a => by rw [Term.subst] | .node cs => by rw [Term.subst] congr 1 conv_rhs => rw [← List.map_id cs] apply List.map_congr_left intro c hc exact Term.subst_none c termination_by t => sizeOf t decreasing_by have ``` #### `Formula.subst_none` ```lean theorem Formula.subst_none : (φ : Formula P A) → φ.subst (fun _ => none) = φ | .atom p terms => by rw [Formula.subst] congr 1 conv_rhs => rw [← List.map_id terms] apply List.map_congr_left intro t _ exact Term.subst_none t | .not f => by rw [Formula.subst, Formula.subst_none f] | .and parts => by rw [Formula.subst_and] congr 1 conv_rhs => rw [← List.map_id parts] apply List.map_congr_left intro g hg exact Formula.subst_none g | .or parts => by rw [Formula.subst_or] congr 1 conv_rhs => rw [← List.map_id parts] apply List.map_congr_left intro g hg exact Formula.subst_none g | .implies a c => by rw [Formula.subst, Formula.subst_none a, Formula.subst_none c] | .all x body => by rw [Formula.subst, Formula.subst_none body] | .exists x body => by rw [Formula.subst, Formula.subst_none body] termination_by φ => sizeOf φ decreasing_by all_goals simp_wf all_goals try (have ``` #### `clauseForm_sound` The clause form of a formula in namespace `ns`: the walk from an empty environment and no universals, then distribution. -/ def clauseForm (ns sep : String) (φ : Formula P A) : List (Clause P A) × Sk := let r := nnf ⟨ns, sep, 0⟩ false [] [] φ (cnf r.1, r.2) /-- **Soundness of the clause form.** Wherever a closed, scoped, well-formed formula that mentions no Skolem name of its namespace is true, some witness functions for the names the walk issues make every clause of its clause form true. ```lean theorem clauseForm_sound (ns sep : String) (φ : Formula P A) (hwf : φ.WF) (hsc : φ.Scoped (fun _ => False)) (hclosed : φ.FV = []) (hnames : ∀ s ∈ φ.names, ¬ (Sk.mk ns sep 0).Fresh s) (M : Structure P A) (hφ : φ.true M) : ∃ fs : String → Option (List M.D → M.D), FreshRange ⟨ns, sep, 0⟩ (clauseForm ns sep φ).2 fs ∧ ∀ c ∈ (clauseForm ns sep φ).1, Clause.true (M.withSkolems fs) c ``` #### `clauseForm_names` **The names of the clause form are the walk's.** A closed, scoped, well-formed formula without witness terms yields clauses whose Skolem names are all issued in the namespace. ```lean theorem clauseForm_names (ns sep : String) (φ : Formula P A) (hwf : φ.WF) (hsc : φ.Scoped (fun _ => False)) (hclosed : φ.FV = []) (hnone : φ.names = []) : ∀ l ∈ (nnf ⟨ns, sep, 0⟩ false [] [] φ).1.lits, ∀ s ∈ l.names, (Sk.mk ns sep 0).Fresh s ``` ### `Sheaf/Resolution.lean` **Soundness of one resolution step** The kernel's `resolve` (`sheaf-kernel/src/resolution_rule.rs`) takes clauses `L` and `R` that share no variable, literals `a` and `b` of opposite sign on the same predicate, computes a unifier `σ` of their terms, and returns `(L' ++ R') σ` where `L'` is `L` without `a` and `R'` is `R` without `b`. The theorem below says that in any structure where `L` and `R` are true, that resolvent is true. It is stated for any `L'` and `R'` that keep every literal other than `a` and `b`, which is exactly what removing by equality does, so it needs no decidable equality on terms. Together with the facts that every leaf of an accepted certificate is a clause of a premise or of the negated target, and that the final clause is empty (true in no structure), this is the soundness of binary mode: the premises and the negated target have no model, so the premises entail the target. #### `resolution_sound` `σ` unifies two literals' arguments when the substituted argument lists are equal. -/ def Unifies [SkolemAtoms A] (σ : Subst A) (a b : Literal P A) : Prop := a.terms.map (Term.subst σ) = b.terms.map (Term.subst σ) /-- Soundness of one resolution step. ```lean theorem resolution_sound [SkolemAtoms A] (M : Structure P A) (L R L' R' : Clause P A) (a b : Literal P A) (σ : Subst A) (hLw : L.WF) (hRw : R.WF) (hL' : ∀ x ∈ L, x ≠ a → x ∈ L') (hR' : ∀ x ∈ R, x ≠ b → x ∈ R') (hsign : a.positive = !b.positive) (hpred : a.pred = b.pred) (hσ : Unifies σ a b) (hL : Clause.true M L) (hR : Clause.true M R) : Clause.true M (Clause.subst σ (L' ++ R')) ``` #### `resolution_sound_collected` The resolvent as the kernel builds it: the two sides are substituted literal by literal, and then collected into one clause that has every one of them (the kernel's set may drop duplicates and reorder). ```lean theorem resolution_sound_collected [SkolemAtoms A] (M : Structure P A) (L R L' R' S : Clause P A) (a b : Literal P A) (σ : Subst A) (hLw : L.WF) (hRw : R.WF) (hL' : ∀ x ∈ L, x ≠ a → x ∈ L') (hR' : ∀ x ∈ R, x ≠ b → x ∈ R') (hS : ∀ x ∈ Clause.subst σ (L' ++ R'), x ∈ S) (hsign : a.positive = !b.positive) (hpred : a.pred = b.pred) (hσ : Unifies σ a b) (hL : Clause.true M L) (hR : Clause.true M R) : Clause.true M S ``` #### `empty_clause_false` The empty clause is true in no structure. ```lean theorem empty_clause_false [SkolemAtoms A] (M : Structure P A) : ¬ Clause.true M ([] : Clause P A) ``` ### `SheafKernel/Soundness.lean` **Soundness of the kernel's resolution step** `resolution_rule.resolve` returns a clause only when it is a resolvent in the sense of `Sheaf.resolution_sound_collected`: every literal of the two sides other than the two resolved on, under the unifier the kernel checked, is in it. So in any structure where the two sides are true, the result is true. #### `literal_apply_loop_error` ```lean theorem literal_apply_loop_error (v : alloc.vec.Vec KTerm) (σ : KSubst) (out out1 : alloc.vec.Vec KTerm) (e : first_order.Malformed) (index : Usize) (error1 : Option first_order.Malformed) (h : first_order.Literal.apply_loop v σ out (some e) index = ok (out1, error1)) : error1 = some e ``` #### `literal_apply_loop_spec` ```lean theorem literal_apply_loop_spec (σ : KSubst) : ∀ (k : Nat) (v out out1 : alloc.vec.Vec KTerm) (index : Usize), v.length - index.val = k → first_order.Literal.apply_loop v σ out none index = ok (out1, none) → out1.val.map termToSpec = out.val.map termToSpec ++ (v.val.drop index.val).map (fun c => (termToSpec c).subst (substOf σ)) ``` #### `literal_apply_spec` `Literal.apply` is substitution by `substOf σ`. ```lean theorem literal_apply_spec (l : KLiteral) (σ : KSubst) (l' : KLiteral) (h : first_order.Literal.apply l σ = ok (.Ok l')) : literalToSpec l' = (literalToSpec l).subst (substOf σ) ``` #### `listOrder_eq` ```lean theorem listOrder_eq {T : Type} (cmp : T → T → Result Ordering) : ∀ (l1 l2 : List T), (∀ x ∈ l1, ∀ y, cmp x y = ok Ordering.eq → x = y) → listOrder cmp l1 l2 = ok Ordering.eq → l1 = l2 ``` #### `literal_cmp_eq` `cmp` on literals answers `Equal` only for equal literals. ```lean theorem literal_cmp_eq (a b : KLiteral) (h : first_order.Literal.Insts.CoreCmpOrd.cmp a b = ok Ordering.eq) : a = b ``` #### `literal_set_insert_mem` Inserting a literal into a set puts it there. ```lean theorem literal_set_insert_mem (s : KClause) (item : KLiteral) (b : Bool) (s' : KClause) (h : sorted_collections.Set.insert first_order.Literal.Insts.CoreCmpOrd s item = ok (b, s')) : (∀ y ∈ s.items.val, y ∈ s'.items.val) ∧ item ∈ s'.items.val ``` #### `apply_clause_loop_error` ```lean theorem apply_clause_loop_error (σ : KSubst) (literals : Slice KLiteral) (out out1 : KClause) (e : first_order.Malformed) (index : Usize) (error1 : Option first_order.Malformed) (h : first_order.apply_clause_loop σ literals out (some e) index = ok (out1, error1)) : error1 = some e ``` #### `apply_clause_loop_spec` ```lean theorem apply_clause_loop_spec (σ : KSubst) : ∀ (k : Nat) (literals : Slice KLiteral) (out out1 : KClause) (index : Usize), literals.length - index.val = k → first_order.apply_clause_loop σ literals out none index = ok (out1, none) → (∀ y ∈ out.items.val, y ∈ out1.items.val) ∧ ∀ j, index.val ≤ j → (hj : j < literals.length) → ∃ l', first_order.Literal.apply literals.val[j] σ = ok (.Ok l') ∧ l' ∈ out1.items.val ``` #### `apply_clause_spec` Every literal of a clause has its substitution instance in `apply_clause`'s result. ```lean theorem apply_clause_spec (c : KClause) (σ : KSubst) (c' : KClause) (h : first_order.apply_clause c σ = ok (.Ok c')) : ∀ x ∈ Sheaf.Clause.subst (substOf σ) (clauseToSpec c), x ∈ clauseToSpec c' ``` #### `add_others_loop_error` ```lean theorem add_others_loop_error (except : KLiteral) (σ : KSubst) (into into1 : KClause) (literals : Slice KLiteral) (e : first_order.Malformed) (index : Usize) (error1 : Option first_order.Malformed) (h : resolution_rule.add_others_loop except σ into literals (some e) index = ok (into1, error1)) : error1 = some e ``` #### `add_others_loop_spec` ```lean theorem add_others_loop_spec (except : KLiteral) (σ : KSubst) : ∀ (k : Nat) (literals : Slice KLiteral) (into into1 : KClause) (index : Usize), literals.length - index.val = k → resolution_rule.add_others_loop except σ into literals none index = ok (into1, none) → (∀ y ∈ into.items.val, y ∈ into1.items.val) ∧ ∀ j, index.val ≤ j → (hj : j < literals.length) → literals.val[j] ≠ except → ∃ l', first_order.Literal.apply literals.val[j] σ = ok (.Ok l') ∧ l' ∈ into1.items.val ``` #### `add_others_spec` ```lean theorem add_others_spec (clause : KClause) (except : KLiteral) (σ : KSubst) (into into1 : KClause) (h : resolution_rule.add_others clause except σ into = ok (.Ok (), into1)) : (∀ y ∈ into.items.val, y ∈ into1.items.val) ∧ ∀ l ∈ clause.items.val, l ≠ except → ∃ l', first_order.Literal.apply l σ = ok (.Ok l') ∧ l' ∈ into1.items.val ``` #### `value_ne_eq_false` ```lean theorem value_ne_eq_false (a b : Value) (h : core.cmp.PartialEq.ne.trait_default canonical_value.Value.Insts.CoreCmpPartialEqValue a b = ok false) : a = b ``` #### `same_under_spec` `same_under` says `true` only when the substitution makes the two terms equal. ```lean theorem same_under_spec (a b : KTerm) (σ : KSubst) (h : resolution_rule.same_under a b σ = ok (.Ok true)) : (termToSpec a).subst (substOf σ) = (termToSpec b).subst (substOf σ) ``` #### `unifies_loop_error` ```lean theorem unifies_loop_error (v v1 : alloc.vec.Vec KTerm) (σ : KSubst) (same same1 : Bool) (e : first_order.Malformed) (index : Usize) (error1 : Option first_order.Malformed) (h : resolution_rule.unifies_loop v v1 σ same (some e) index = ok (same1, error1)) : error1 = some e ``` #### `unifies_loop_spec` ```lean theorem unifies_loop_spec (σ : KSubst) : ∀ (k : Nat) (v v1 : alloc.vec.Vec KTerm) (same : Bool) (index : Usize), v.length - index.val = k → resolution_rule.unifies_loop v v1 σ same none index = ok (true, none) → same = true ∧ ∀ j, index.val ≤ j → (hj : j < v.length) → (hj1 : j < v1.length) → (termToSpec v.val[j]).subst (substOf σ) = (termToSpec v1.val[j]).subst (substOf σ) ``` #### `unifies_spec` The kernel's unifier check means the spec's `Unifies`. ```lean theorem unifies_spec (left right : KLiteral) (σ : KSubst) (h : resolution_rule.unifies left right σ = ok (.Ok true)) : Sheaf.Unifies (substOf σ) (literalToSpec left) (literalToSpec right) ``` #### `bind_err_ne_ok` Building an error after one bind never yields `Ok`. ```lean theorem bind_err_ne_ok {α β E : Type} (m : Result α) (f : α → E) (v : β) : (Bind.bind m (fun s => ok (core.result.Result.Err (f s))) : Result (core.result.Result β E)) ≠ ok (.Ok v) ``` #### `literal_sign_opposite` Opposite signs, read in the spec. ```lean theorem literal_sign_opposite (a b : KLiteral) (h : ¬ a.positive = b.positive) : (literalToSpec a).positive = !(literalToSpec b).positive ``` #### `from_residual_malformed_ne_ok` A `Break` residual of a `Malformed` error never yields `Ok`. ```lean theorem from_residual_malformed_ne_ok (e : first_order.Malformed) (r : KClause) (h : core.result.Result.Insts.CoreOpsTry_traitFromResidualResult.from_residual (sorted_collections.Set first_order.Literal) resolution_rule.StepError.Insts.CoreConvertFromMalformed (core.result.Result.Err e) = ok (.Ok r)) : False ``` #### `resolve_sound` **Soundness of the kernel's resolution step.** When `resolve` returns a clause, that clause is true in every structure where the two sides are true. ```lean theorem resolve_sound (left right : KClause) (on_left on_right : KLiteral) («prefix» : Str) (r : KClause) (h : resolution_rule.resolve left right on_left on_right «prefix» = ok (.Ok r)) (M : Sheaf.Structure Value Value) (hleft : (clauseToSpec left).true M) (hright : (clauseToSpec right).true M) : (clauseToSpec r).true M ``` ### `SheafKernel/Certificates.lean` **Soundness of the certificate walk, at the clause level** `certificate_check` loads the declared clauses of every premise and of the goal as leaves, replays every step, and demands that the conclusion be the empty clause. Here we show what the replay guarantees about clauses: every clause the kernel registers is a consequence of the leaves, so an accepted conclusion means the leaves have no model, unless an `identity` step was accepted. The identity step rests on the semantic hash (two trees with the same hash are the same statement), which is not a clause-level fact; it is accounted for separately. #### `set_clone_eq` `c` follows from `leaves`: it is true in every structure where they all are. -/ def Consequence (leaves : List KClause) (c : KClause) : Prop := ∀ M : Sheaf.Structure Value Value, (∀ l ∈ leaves, (clauseToSpec l).true M) → (clauseToSpec c).true M /-- The leaves have no model. -/ def Unsat (leaves : List KClause) : Prop := ∀ M : Sheaf.Structure Value Value, ¬ ∀ l ∈ leaves, (clauseToSpec l).true M /-- The clauses a map holds, whatever their keys. -/ def values (m : KMap) : List KClause := m.entries.val.map Prod.snd /-- Every clause in the map follows from the leaves. -/ def MapSound (leaves : List KClause) (m : KMap) : Prop := ∀ c ∈ values m, Consequence leaves c theorem consequence_of_leaf (leaves : List KClause) (c : KClause) (h : c ∈ leaves) : Consequence leaves c := fun _ hM => hM c h theorem consequence_resolve (leaves : List KClause) (left right : KClause) (on_left on_right : KLiteral) («prefix» : Str) (r : KClause) (h : resolution_rule.resolve left right on_left on_right «prefix» = ok (.Ok r)) (hl : Consequence leaves left) (hr : Consequence leaves right) : Consequence leaves r := fun M hM => resolve_sound left right on_left on_right «prefix» r h M (hl M hM) (hr M hM) theorem unsat_of_empty_consequence (leaves : List KClause) (c : KClause) (hc : Consequence leaves c) (hempty : c.items.val = []) : Unsat leaves := by intro M hM have := hc M hM unfold clauseToSpec at this rw [hempty] at this exact Sheaf.empty_clause_false M this /-! ## Maps: what `cloned` returns is a value, what `insert` adds is the new value ```lean theorem set_clone_eq (s s' : KClause) (h : sorted_collections.Set.Insts.CoreCloneClone.clone first_order.Literal.Insts.CoreCloneClone s = ok s') : s' = s ``` #### `map_cloned_mem` ```lean theorem map_cloned_mem {Q : Type} (inst1 : core.cmp.Ord Q) (binst : core.borrow.Borrow String Q) (m : KMap) (key : Q) (c : KClause) (h : sorted_collections.Map.cloned alloc.string.String.Insts.CoreCmpOrd inst1 binst (sorted_collections.Set.Insts.CoreCloneClone first_order.Literal.Insts.CoreCloneClone) m key = ok (some c)) : c ∈ values m ``` #### `map_insert_values` ```lean theorem map_insert_values (m : KMap) (k : String) (v : KClause) (p : Option KClause × KMap) (h : sorted_collections.Map.insert alloc.string.String.Insts.CoreCmpOrd m k v = ok p) : ∀ c ∈ values p.2, c = v ∨ c ∈ values m ``` #### `map_insert_entries` After `insert`, every entry is an old one or carries the inserted value. ```lean theorem map_insert_entries {V : Type} (m : sorted_collections.Map String V) (k : String) (v : V) (p : Option V × sorted_collections.Map String V) (h : sorted_collections.Map.insert alloc.string.String.Insts.CoreCmpOrd m k v = ok p) : ∀ e ∈ p.2.entries.val, e.2 = v ∨ e ∈ m.entries.val ``` #### `map_cloned_string_mem` What `cloned` finds in a string map is the value of one of its entries. ```lean theorem map_cloned_string_mem (m : sorted_collections.Map String String) (key : String) (s : String) (h : sorted_collections.Map.cloned alloc.string.String.Insts.CoreCmpOrd alloc.string.String.Insts.CoreCmpOrd (core.borrow.Borrow.Blanket String) alloc.string.String.Insts.CoreCloneClone m key = ok (some s)) : ∃ e ∈ m.entries.val, e.2 = s ``` #### `map_insert_sound` ```lean theorem map_insert_sound (leaves : List KClause) (m : KMap) (k : String) (v : KClause) (p : Option KClause × KMap) (h : sorted_collections.Map.insert alloc.string.String.Insts.CoreCmpOrd m k v = ok p) (hm : MapSound leaves m) (hv : Consequence leaves v) : MapSound leaves p.2 ``` #### `map_new_values` ```lean theorem map_new_values (m : KMap) (h : sorted_collections.Map.new KClause alloc.string.String.Insts.CoreCmpOrd = ok m) : values m = [] ``` #### `from_residual_err` A `Break` residual carries an error. ```lean theorem from_residual_err {T E : Type} (residual : core.result.Result Never E) (rr : core.result.Result T E) (h : core.result.Result.Insts.CoreOpsTry_traitFromResidualResult.from_residual T (core.convert.FromSame E) residual = ok rr) : ∃ e, rr = .Err e ``` #### `identity_step_spec` `check_step` accepted an `identity` step, with these arguments. -/ def IdentityStep (step : Value) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) (clauses : KMap) (depths : sorted_collections.Map String Usize) (derived : alloc.vec.Vec (String × KClause)) (out : KMap × sorted_collections.Map String Usize × alloc.vec.Vec (String × KClause)) : Prop := ∃ id, certificate_check.check_identity_step step id goal_hash premise_hashes clauses depths derived = ok (.Ok (), out) /-- Continue past a `?` whose operand was `Ok`. -/ syntax "continue_step" ident ident : tactic macro_rules | `(tactic| continue_step $hcf:ident $h:ident) => `(tactic| (simp only [core.result.Result.Insts.CoreOpsTry.branch, ok_eq_ok_iff] at $hcf:ident subst $hcf:ident dsimp only at $h:ident)) /-- A `?` whose operand was `Err` cannot have produced `Ok`. -/ syntax "break_step" ident ident : tactic macro_rules | `(tactic| break_step $hcf:ident $h:ident) => `(tactic| (simp only [core.result.Result.Insts.CoreOpsTry.branch, ok_eq_ok_iff] at $hcf:ident subst $hcf:ident dsimp only at $h:ident read_ok at $h:ident obtain ⟨rr, hrr, $h:ident⟩ := $h:ident obtain ⟨e', he'⟩ := from_residual_err _ _ hrr subst he' simp at $h:ident)) /-- A branch that builds an error cannot have produced `Ok`. -/ syntax "err_step" ident : tactic macro_rules | `(tactic| err_step $h:ident) => `(tactic| (try simp only [↓reduceIte, Bool.false_eq_true] at $h:ident first | (read_ok at $h:ident; simp at $h:ident) | simp at $h:ident)) /-- An accepted `identity` step was given a non-empty goal hash, and names a premise whose recorded hash is that goal hash. ```lean theorem identity_step_spec (step : Value) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) (clauses : KMap) (depths : sorted_collections.Map String Usize) (derived : alloc.vec.Vec (String × KClause)) (out : KMap × sorted_collections.Map String Usize × alloc.vec.Vec (String × KClause)) (h : IdentityStep step goal_hash premise_hashes clauses depths derived out) : goal_hash.val ≠ [] ∧ ∃ (hash : String) (s : Str), (∃ e ∈ premise_hashes.entries.val, e.2 = hash) ∧ strOf hash = ok s ∧ s.val = goal_hash.val ``` #### `step_clause_mem` ```lean theorem step_clause_mem (clauses : KMap) (id reference : Str) (c : KClause) (h : certificate_check.step_clause clauses id reference = ok (.Ok c)) : c ∈ values clauses ``` #### `check_step_sound` One accepted step keeps every registered clause a consequence of the leaves, unless it was an `identity` step. ```lean theorem check_step_sound (leaves : List KClause) (step : Value) (index : Usize) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) (clauses : KMap) (depths : sorted_collections.Map String Usize) (derived : alloc.vec.Vec (String × KClause)) (clauses1 : KMap) (depths1 : sorted_collections.Map String Usize) (derived1 : alloc.vec.Vec (String × KClause)) (hm : MapSound leaves clauses) (h : certificate_check.check_step step index goal_hash premise_hashes clauses depths derived = ok (.Ok (), clauses1, depths1, derived1)) : MapSound leaves clauses1 ∨ IdentityStep step goal_hash premise_hashes clauses depths derived (clauses1, depths1, derived1) ``` #### `check_conclusion_sound` An `identity` step was accepted somewhere in the list, against this goal hash and these premise hashes (which the walk never changes). -/ def IdentityUsed (steps : Slice Value) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) : Prop := ∃ step ∈ steps.val, ∃ (clauses : KMap) (depths : sorted_collections.Map String Usize) (derived : alloc.vec.Vec (String × KClause)) (out : KMap × sorted_collections.Map String Usize × alloc.vec.Vec (String × KClause)), IdentityStep step goal_hash premise_hashes clauses depths derived out theorem identity_used_spec (steps : Slice Value) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) (h : IdentityUsed steps goal_hash premise_hashes) : goal_hash.val ≠ [] ∧ ∃ (hash : String) (s : Str), (∃ e ∈ premise_hashes.entries.val, e.2 = hash) ∧ strOf hash = ok s ∧ s.val = goal_hash.val := by obtain ⟨step, _, clauses, depths, derived, out, hstep⟩ := h exact identity_step_spec step goal_hash premise_hashes clauses depths derived out hstep theorem check_steps_loop_error (steps : Slice Value) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) (clauses : KMap) (depths : sorted_collections.Map String Usize) (derived : alloc.vec.Vec (String × KClause)) (v : certificate_check.Verdict) (index : Usize) (out : KMap × sorted_collections.Map String Usize × alloc.vec.Vec (String × KClause) × Option certificate_check.Verdict) (h : certificate_check.check_steps_loop steps goal_hash premise_hashes clauses depths derived (some v) index = ok out) : out.2.2.2 = some v := by unfold certificate_check.check_steps_loop at h dsimp only at h split at h · simp only [core.option.Option.is_none] at h split at h · rename_i hb exact absurd hb (by simp) · rw [ok_eq_ok_iff] at h rw [← h] · rw [ok_eq_ok_iff] at h rw [← h] theorem check_steps_loop_sound (leaves : List KClause) : ∀ (k : Nat) (steps : Slice Value) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) (clauses : KMap) (depths : sorted_collections.Map String Usize) (derived : alloc.vec.Vec (String × KClause)) (index : Usize) (out : KMap × sorted_collections.Map String Usize × alloc.vec.Vec (String × KClause) × Option certificate_check.Verdict), steps.length - index.val = k → MapSound leaves clauses → certificate_check.check_steps_loop steps goal_hash premise_hashes clauses depths derived none index = ok out → out.2.2.2 = none → MapSound leaves out.1 ∨ IdentityUsed steps goal_hash premise_hashes := by intro k induction k with | zero => intro steps goal_hash premise_hashes clauses depths derived index out hk hm h hnone unfold certificate_check.check_steps_loop at h dsimp only at h split at h · exfalso scalar_tac · rw [ok_eq_ok_iff] at h rw [← h] exact Or.inl hm | succ k ihk => intro steps goal_hash premise_hashes clauses depths derived index out hk hm h hnone unfold certificate_check.check_steps_loop at h dsimp only at h split at h · rename_i hlt rw [if_pos (show core.option.Option.is_none (none : Option certificate_check.Verdict) = true from rfl)] at h read_ok at h obtain ⟨v, hv, q, hq, failure1, hfail, h⟩ := h have hidx : (core.num.Usize.wrapping_add index 1#usize).val = index.val + 1 := usize_succ_val index steps.length (by scalar_tac) steps.property have hv' := slice_index_usize_eq_ok _ _ _ hv cases hq1 : q.1 with | Err verdict => rw [hq1] at hfail dsimp only at hfail rw [ok_eq_ok_iff] at hfail subst hfail exfalso have := check_steps_loop_error _ _ _ _ _ _ _ _ _ h rw [hnone] at this exact absurd this (by simp) | Ok u => rw [hq1] at hfail dsimp only at hfail rw [ok_eq_ok_iff] at hfail subst hfail have hq' : certificate_check.check_step v index goal_hash premise_hashes clauses depths derived = ok (.Ok (), q.2.1, q.2.2.1, q.2.2.2) := by have hqq : q = (.Ok (), q.2.1, q.2.2.1, q.2.2.2) := by cases u exact Prod.ext hq1 rfl rw [hqq] at hq exact hq rcases check_step_sound leaves v index goal_hash premise_hashes clauses depths derived _ _ _ hm hq' with hsound | hid · exact ihk steps goal_hash premise_hashes q.2.1 q.2.2.1 q.2.2.2 (core.num.Usize.wrapping_add index 1#usize) out (by omega) hsound h hnone · right exact ⟨v, List.mem_of_getElem? hv', clauses, depths, derived, _, hid⟩ · exfalso scalar_tac theorem check_steps_sound (leaves : List KClause) (steps : Slice Value) (goal_hash : Str) (premise_hashes : sorted_collections.Map String String) (clauses : KMap) (depths : sorted_collections.Map String Usize) (derived : alloc.vec.Vec (String × KClause)) (clauses1 : KMap) (depths1 : sorted_collections.Map String Usize) (derived1 : alloc.vec.Vec (String × KClause)) (hm : MapSound leaves clauses) (h : certificate_check.check_steps steps goal_hash premise_hashes clauses depths derived = ok (.Ok (), clauses1, depths1, derived1)) : MapSound leaves clauses1 ∨ IdentityUsed steps goal_hash premise_hashes := by unfold certificate_check.check_steps at h read_ok at h obtain ⟨out, hout, h⟩ := h cases hfail : out.2.2.2 with | some verdict => rw [hfail] at h; simp at h | none => rw [hfail] at h dsimp only at h rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq, true_and] at h obtain ⟨hc, _, _⟩ := h rw [← hc] exact check_steps_loop_sound leaves _ steps goal_hash premise_hashes clauses depths derived _ out rfl hm hout hfail /-! ## The conclusion ```lean theorem check_conclusion_sound (leaves : List KClause) (clauses : KMap) (conclusion : Str) (hm : MapSound leaves clauses) (h : certificate_check.check_conclusion clauses conclusion = ok (.Ok ())) : Unsat leaves ``` #### `check_inner_sound` A direct `?` failure in `check_inner` cannot have produced `Ok`. -/ syntax "break_direct" ident ident : tactic macro_rules | `(tactic| break_direct $hcf:ident $h:ident) => `(tactic| (simp only [core.result.Result.Insts.CoreOpsTry.branch, ok_eq_ok_iff] at $hcf:ident subst $hcf:ident dsimp only at $h:ident obtain ⟨e', he'⟩ := from_residual_err _ _ $h:ident simp at he')) /-- **Soundness of the certificate walk, at the clause level.** An accepted certificate's leaf clauses (the premises' declared clauses, and the goal's unless the answer is `inconsistent`) have no model, unless an `identity` step was accepted against the identity hash: the goal's hash for a proof, empty otherwise. ```lean theorem check_inner_sound (cert : Value) (v : certificate_check.Verdict) (h : certificate_check.check_inner cert = ok (.Ok v)) : ∃ (profile : working_graph.Profile) (premises : alloc.vec.Vec Value) (clauses1 leaves : KMap) (ph1 : sorted_collections.Map String String) (steps : alloc.vec.Vec Value) (identity : String) (identityS : Str), certificate_check.read_profile cert = ok (.Ok profile) ∧ certificate_check.list_field cert (toStr "premises") (toStr "premises") = ok (.Ok premises) ∧ certificate_check.check_premises (alloc.vec.Vec.deref premises) profile { entries ``` ### `SheafKernel/ClauseForm.lean` **The kernel's clause form computes the specification's** `clause_form::clauses` checks the formula (`formula_ok`), walks it into negation normal form while Skolemizing (`Skolemizer::nnf`), and distributes into clauses (`cnf`). Here we relate each kernel step to the pure algorithm of `Sheaf/ClauseForm.lean` and `Sheaf/Cnf.lean`, whose soundness is proved there. The environment of bound variables is a sorted map. The relation `EnvRel` between it and the specification's association list asks only what a successful lookup returns, and the kernel checks (`any_mentions_bound`) that no bound variable survives substitution, so no proof here rests on the map's search being complete. #### `envRel_insert` A kernel formula as a spec formula. -/ def formulaToSpec : clause_form.Formula → Sheaf.Formula Value Value | .Atom p terms => .atom p (terms.val.map termToSpec) | .Not f => .not (formulaToSpec f) | .And parts => .and (parts.val.attach.map (fun (f : {f // f ∈ parts.val}) => formulaToSpec f.val)) | .Or parts => .or (parts.val.attach.map (fun (f : {f // f ∈ parts.val}) => formulaToSpec f.val)) | .Implies a c => .implies (formulaToSpec a) (formulaToSpec c) | .All x body => .all x (formulaToSpec body) | .Exists x body => .exists x (formulaToSpec body) termination_by f => sizeOf f decreasing_by all_goals simp_wf all_goals try (have h1 := List.sizeOf_lt_of_mem f.property) all_goals try (have h2 := Vec.sizeOf_val_lt parts) all_goals omega theorem formulaToSpec_atom (p : Value) (terms : alloc.vec.Vec KTerm) : formulaToSpec (.Atom p terms) = .atom p (terms.val.map termToSpec) := by rw [formulaToSpec] theorem formulaToSpec_not (f : clause_form.Formula) : formulaToSpec (.Not f) = .not (formulaToSpec f) := by rw [formulaToSpec] theorem formulaToSpec_and (parts : alloc.vec.Vec clause_form.Formula) : formulaToSpec (.And parts) = .and (parts.val.map formulaToSpec) := by rw [formulaToSpec] simp theorem formulaToSpec_or (parts : alloc.vec.Vec clause_form.Formula) : formulaToSpec (.Or parts) = .or (parts.val.map formulaToSpec) := by rw [formulaToSpec] simp theorem formulaToSpec_implies (a c : clause_form.Formula) : formulaToSpec (.Implies a c) = .implies (formulaToSpec a) (formulaToSpec c) := by rw [formulaToSpec] theorem formulaToSpec_all (x : String) (body : clause_form.Formula) : formulaToSpec (.All x body) = .all x (formulaToSpec body) := by rw [formulaToSpec] theorem formulaToSpec_exists (x : String) (body : clause_form.Formula) : formulaToSpec (.Exists x body) = .exists x (formulaToSpec body) := by rw [formulaToSpec] /-- A kernel negation normal form as a spec one. -/ def nnfToSpec : clause_form.Nnf → Sheaf.Nnf Value Value | .Literal l => .lit (literalToSpec l) | .And parts => .and (parts.val.attach.map (fun (n : {n // n ∈ parts.val}) => nnfToSpec n.val)) | .Or parts => .or (parts.val.attach.map (fun (n : {n // n ∈ parts.val}) => nnfToSpec n.val)) termination_by n => sizeOf n decreasing_by all_goals simp_wf all_goals try (have h1 := List.sizeOf_lt_of_mem n.property) all_goals try (have h2 := Vec.sizeOf_val_lt parts) all_goals omega theorem nnfToSpec_lit (l : KLiteral) : nnfToSpec (.Literal l) = .lit (literalToSpec l) := by rw [nnfToSpec] theorem nnfToSpec_and (parts : alloc.vec.Vec clause_form.Nnf) : nnfToSpec (.And parts) = .and (parts.val.map nnfToSpec) := by rw [nnfToSpec] simp theorem nnfToSpec_or (parts : alloc.vec.Vec clause_form.Nnf) : nnfToSpec (.Or parts) = .or (parts.val.map nnfToSpec) := by rw [nnfToSpec] simp /-! ## The environment -/ /-- The kernel map and the spec association list bind the same variables to the same terms. -/ def EnvRel (σ : KEnv) (E : Sheaf.Env Value) : Prop := ∀ x t, E.find x = some t ↔ ∃ e ∈ σ.entries.val, e.1 = x ∧ termToSpec e.2 = t /-- A variable is a key of the map. -/ def IsKey (σ : KEnv) (y : String) : Prop := ∃ e ∈ σ.entries.val, e.1 = y theorem envRel_find_none {σ : KEnv} {E : Sheaf.Env Value} (h : EnvRel σ E) (x : String) (hx : ¬ IsKey σ x) : E.find x = none := by cases hf : E.find x with | none => rfl | some t => obtain ⟨e, he, hex, _⟩ := (h x t).mp hf exact absurd ⟨e, he, hex⟩ hx theorem envRel_find_mem {σ : KEnv} {E : Sheaf.Env Value} (h : EnvRel σ E) (x : String) (t : KTerm) (hm : (x, t) ∈ σ.entries.val) : E.find x = some (termToSpec t) := (h x (termToSpec t)).mpr ⟨(x, t), hm, rfl, rfl⟩ theorem envRel_nil (σ : KEnv) (h : σ.entries.val = []) : EnvRel σ [] := by intro x t rw [h] simp [Sheaf.Env.find] /-- Inserting a new key extends the association list at the front. ```lean theorem envRel_insert {σ σ' : KEnv} {E : Sheaf.Env Value} (h : EnvRel σ E) (x : String) (w : KTerm) (hnew : ¬ IsKey σ x) (hins : ∀ e, e ∈ σ'.entries.val ↔ e = (x, w) ∨ e ∈ σ.entries.val) : EnvRel σ' ((x, termToSpec w) :: E) ``` #### `u32_pos_of_checked_sub` ```lean theorem u32_pos_of_checked_sub (f g : U32) (h : U32.checked_sub f 1#u32 = some g) : g.val + 1 = f.val ``` #### `apply_fuel_loop_rel` The loop of `apply_fuel` records, for every child from `index` on, the result of `apply_fuel` at the same fuel. ```lean theorem apply_fuel_loop_rel (σ : KSubst) (f : U32) : ∀ (k : Nat) (children out out1 : alloc.vec.Vec KTerm) (index : Usize), children.length - index.val = k → first_order.apply_fuel_loop children σ f out none index = ok (out1, none) → ∃ us, out1.val = out.val ++ us ∧ List.Forall₂ (fun t u => first_order.apply_fuel t σ f = ok (.Ok u)) (children.val.drop index.val) us ``` #### `forall₂_map_eq` ```lean theorem forall₂_map_eq {R : KTerm → KTerm → Prop} (g : KTerm → STerm) : ∀ (ts us : List KTerm), List.Forall₂ R ts us → (∀ t u, R t u → t ∈ ts → u ∈ us → termToSpec u = g t) → us.map termToSpec = ts.map g ``` #### `apply_fuel_fixed` Applying the map to a term none of whose variables it binds returns the term. ```lean theorem apply_fuel_fixed : ∀ (n : Nat) (t : KTerm) (σ : KEnv) (f : U32) (u : KTerm), f.val = n → (∀ y ∈ (termToSpec t).vars, ¬ IsKey σ y) → first_order.apply_fuel t σ f = ok (.Ok u) → termToSpec u = termToSpec t ``` #### `apply_fuel_env` Values of the environment mention no bound variable. -/ def ValsFree (σ : KEnv) : Prop := ∀ e ∈ σ.entries.val, ∀ y ∈ (termToSpec e.2).vars, ¬ IsKey σ y /-- When the result mentions no bound variable, `apply_fuel` is the spec's single-pass substitution by the environment. ```lean theorem apply_fuel_env : ∀ (n : Nat) (t : KTerm) (σ : KEnv) (E : Sheaf.Env Value) (f : U32) (u : KTerm), f.val = n → EnvRel σ E → ValsFree σ → first_order.apply_fuel t σ f = ok (.Ok u) → (∀ y ∈ (termToSpec u).vars, ¬ IsKey σ y) → termToSpec u = (termToSpec t).subst E.subst ``` #### `apply_env` ```lean theorem apply_env (t : KTerm) (σ : KEnv) (E : Sheaf.Env Value) (u : KTerm) (hrel : EnvRel σ E) (hvals : ValsFree σ) (h : first_order.apply t σ = ok (.Ok u)) (hfree : ∀ y ∈ (termToSpec u).vars, ¬ IsKey σ y) : termToSpec u = (termToSpec t).subst E.subst ``` #### `apply_all_loop_error` ```lean theorem apply_all_loop_error (terms : Slice KTerm) (σ : KEnv) (out out1 : alloc.vec.Vec KTerm) (e : first_order.Malformed) (index : Usize) (error1 : Option first_order.Malformed) (h : clause_form.apply_all_loop terms σ out (some e) index = ok (out1, error1)) : error1 = some e ``` #### `apply_all_loop_rel` ```lean theorem apply_all_loop_rel (σ : KEnv) : ∀ (k : Nat) (terms : Slice KTerm) (out out1 : alloc.vec.Vec KTerm) (index : Usize), terms.length - index.val = k → clause_form.apply_all_loop terms σ out none index = ok (out1, none) → ∃ us, out1.val = out.val ++ us ∧ List.Forall₂ (fun t u => first_order.apply t σ = ok (.Ok u)) (terms.val.drop index.val) us ``` #### `apply_all_rel` ```lean theorem apply_all_rel (terms : Slice KTerm) (σ : KEnv) (us : alloc.vec.Vec KTerm) (h : clause_form.apply_all terms σ = ok (.Ok us)) : List.Forall₂ (fun t u => first_order.apply t σ = ok (.Ok u)) terms.val us.val ``` #### `mentions_bound_loop_found` ```lean theorem mentions_bound_loop_found (children : alloc.vec.Vec KTerm) (σ : KEnv) (f : U32) (error : Option first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.mentions_bound_loop children σ f true error index = ok (b, error1)) : b = true ``` #### `mentions_bound_loop_error` ```lean theorem mentions_bound_loop_error (children : alloc.vec.Vec KTerm) (σ : KEnv) (f : U32) (found : Bool) (e : first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.mentions_bound_loop children σ f found (some e) index = ok (b, error1)) : error1 = some e ``` #### `mentions_bound_loop_all` A loop that ends unfound and without error saw every child return `false`. ```lean theorem mentions_bound_loop_all (children : alloc.vec.Vec KTerm) (σ : KEnv) (f : U32) : ∀ (k : Nat) (index : Usize), children.length - index.val = k → clause_form.mentions_bound_loop children σ f false none index = ok (false, none) → ∀ c ∈ children.val.drop index.val, clause_form.mentions_bound c σ f = ok (.Ok false) ``` #### `mentions_bound_spec` A term `mentions_bound` clears has no variable bound in the environment. ```lean theorem mentions_bound_spec : ∀ (n : Nat) (t : KTerm) (σ : KEnv) (f : U32), f.val = n → clause_form.mentions_bound t σ f = ok (.Ok false) → ∀ y ∈ (termToSpec t).vars, ¬ IsKey σ y ``` #### `any_mentions_bound_loop_found` ```lean theorem any_mentions_bound_loop_found (terms : Slice KTerm) (σ : KEnv) (error : Option first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.any_mentions_bound_loop terms σ true error index = ok (b, error1)) : b = true ``` #### `any_mentions_bound_loop_error` ```lean theorem any_mentions_bound_loop_error (terms : Slice KTerm) (σ : KEnv) (found : Bool) (e : first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.any_mentions_bound_loop terms σ found (some e) index = ok (b, error1)) : error1 = some e ``` #### `any_mentions_bound_loop_all` ```lean theorem any_mentions_bound_loop_all (terms : Slice KTerm) (σ : KEnv) : ∀ (k : Nat) (index : Usize), terms.length - index.val = k → clause_form.any_mentions_bound_loop terms σ false none index = ok (false, none) → ∀ t ∈ terms.val.drop index.val, clause_form.mentions_bound t σ clause_form.FORMULA_FUEL = ok (.Ok false) ``` #### `any_mentions_bound_spec` Terms `any_mentions_bound` clears have no variable bound in the environment. ```lean theorem any_mentions_bound_spec (terms : Slice KTerm) (σ : KEnv) (h : clause_form.any_mentions_bound terms σ = ok (.Ok false)) : ∀ t ∈ terms.val, ∀ y ∈ (termToSpec t).vars, ¬ IsKey σ y ``` ### `SheafKernel/FormulaOk.lean` **What `formula_ok` establishes** Before the walk, `clause_form::clauses` checks the formula: every atom's terms are well-formed and mention only bound variables, every binder introduces a variable not bound around it, and no term carries a witness name of the namespace the walk will issue names from. These are exactly the hypotheses of the pure soundness theorem `clauseForm_sound`, so here we read them off the kernel's check. #### `termToSpec_eq_atom` ```lean theorem termToSpec_eq_atom (c : KTerm) (a : Value) (h : termToSpec c = .atom a) : c = .Atom a ``` #### `termToSpec_eq_node` ```lean theorem termToSpec_eq_node (c : KTerm) (l : List STerm) (h : termToSpec c = .node l) : ∃ cs, c = .Node cs ∧ cs.val.map termToSpec = l ``` #### `skolemName_some` What the spec reads as a witness, and its name. ```lean theorem skolemName_some (cs : List STerm) (s : String) (args : List STerm) (h : Sheaf.skolemName cs = some (s, args)) : cs = [.atom (.Text "skolem"), .atom (.Text s), .node args] ``` #### `is_text_atom_spec` ```lean theorem is_text_atom_spec (t : KTerm) (s : String) (hs : s.toByteArray.size ≤ U32.max) (b : Bool) (h : clause_form.is_text_atom t (toStr s hs) = ok b) : b = true ↔ t = .Atom (.Text s) ``` #### `is_node_spec` ```lean theorem is_node_spec (t : KTerm) (b : Bool) (h : clause_form.is_node t = ok b) : b = true ↔ ∃ cs, t = .Node cs ``` #### `is_text_spec` ```lean theorem is_text_spec (t : KTerm) (b : Bool) (h : clause_form.is_text t = ok b) : b = true ↔ ∃ s, t = .Atom (.Text s) ``` #### `is_witness_shape` On a witness-shaped tuple, `is_witness` says so. ```lean theorem is_witness_shape (cs : Slice KTerm) (b : Bool) (h : clause_form.is_witness cs = ok b) (s : String) (args : alloc.vec.Vec KTerm) (hcs : cs.val = [.Atom (.Text "skolem"), .Atom (.Text s), .Node args]) : b = true ``` #### `names_ok_loop_false` ```lean theorem names_ok_loop_false (children : alloc.vec.Vec KTerm) (f : U32) (error : Option first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.names_ok_loop children f false error index = ok (b, error1)) : b = false ``` #### `names_ok_loop_error` ```lean theorem names_ok_loop_error (children : alloc.vec.Vec KTerm) (f : U32) (ok1 : Bool) (e : first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.names_ok_loop children f ok1 (some e) index = ok (b, error1)) : error1 = some e ``` #### `names_ok_loop_all` ```lean theorem names_ok_loop_all (children : alloc.vec.Vec KTerm) (f : U32) : ∀ (k : Nat) (index : Usize), children.length - index.val = k → clause_form.names_ok_loop children f true none index = ok (true, none) → ∀ c ∈ children.val.drop index.val, clause_form.names_ok c f = ok (.Ok true) ``` #### `names_ok_spec` ```lean theorem names_ok_spec : ∀ (n : Nat) (t : KTerm) (f : U32), f.val = n → clause_form.names_ok t f = ok (.Ok true) → ∀ s ∈ (termToSpec t).names, False ``` #### `variables_listed_loop_false` ```lean theorem variables_listed_loop_false (children : alloc.vec.Vec KTerm) (bound : Slice String) (f : U32) (error : Option first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.variables_listed_loop children bound f false error index = ok (b, error1)) : b = false ``` #### `variables_listed_loop_error` ```lean theorem variables_listed_loop_error (children : alloc.vec.Vec KTerm) (bound : Slice String) (f : U32) (ok1 : Bool) (e : first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.variables_listed_loop children bound f ok1 (some e) index = ok (b, error1)) : error1 = some e ``` #### `variables_listed_loop_all` ```lean theorem variables_listed_loop_all (children : alloc.vec.Vec KTerm) (bound : Slice String) (f : U32) : ∀ (k : Nat) (index : Usize), children.length - index.val = k → clause_form.variables_listed_loop children bound f true none index = ok (true, none) → ∀ c ∈ children.val.drop index.val, clause_form.variables_listed c bound f = ok (.Ok true) ``` #### `variables_listed_spec` ```lean theorem variables_listed_spec : ∀ (n : Nat) (t : KTerm) (bound : Slice String) (f : U32), f.val = n → clause_form.variables_listed t bound f = ok (.Ok true) → ∀ y ∈ (termToSpec t).vars, y ∈ bound.val ``` #### `atom_term_ok_spec` ```lean theorem atom_term_ok_spec (t : KTerm) (bound : Slice String) (h : clause_form.atom_term_ok t bound = ok (.Ok true)) : (termToSpec t).WF ∧ (∀ y ∈ (termToSpec t).vars, y ∈ bound.val) ∧ ∀ s ∈ (termToSpec t).names, False ``` #### `formulaOk_binder` What `formula_ok` establishes of a formula under the bound variables `bound`: well-formed, scoped, closed under `bound`, and carrying no witness term. -/ structure FormulaOk (bound : List String) (φ : Sheaf.Formula Value Value) : Prop where wf : φ.WF binders : φ.Scoped (· ∈ bound) fv : ∀ z ∈ φ.FV, z ∈ bound names : ∀ s ∈ φ.names, False theorem formula_ok_loop_false (terms : alloc.vec.Vec KTerm) (bound : Slice String) (error : Option first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.formula_ok_loop terms bound false error index = ok (b, error1)) : b = false := by unfold clause_form.formula_ok_loop at h dsimp only at h split at h · rw [if_neg (by simp)] at h rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.1.symm · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.1.symm theorem formula_ok_loop_error (terms : alloc.vec.Vec KTerm) (bound : Slice String) (ok1 : Bool) (e : first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.formula_ok_loop terms bound ok1 (some e) index = ok (b, error1)) : error1 = some e := by unfold clause_form.formula_ok_loop at h dsimp only at h split at h · split at h · rw [if_neg (by simp)] at h rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.2.symm · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.2.symm · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.2.symm theorem formula_ok_loop_all (terms : alloc.vec.Vec KTerm) (bound : Slice String) : ∀ (k : Nat) (index : Usize), terms.length - index.val = k → clause_form.formula_ok_loop terms bound true none index = ok (true, none) → ∀ t ∈ terms.val.drop index.val, clause_form.atom_term_ok t bound = ok (.Ok true) := by intro k induction k using Nat.strong_induction_on with | _ k ih => intro index hk h unfold clause_form.formula_ok_loop at h dsimp only at h split at h · rename_i hlt rw [if_pos rfl] at h rw [if_pos (show core.option.Option.is_none (none : Option first_order.Malformed) = true from rfl)] at h read_ok at h obtain ⟨t, ht, r, hr, p, hp, h⟩ := h rw [alloc.vec.Vec.index_slice_index] at ht have ht' := vec_index_usize_eq_ok _ _ _ ht have hlen : terms.length = terms.val.length := rfl have hlt' : index.val < terms.val.length := by scalar_tac have hidx : (core.num.Usize.wrapping_add index 1#usize).val = index.val + 1 := usize_succ_val index terms.length hlt' terms.property have hget : terms.val[index.val] = t := by have := List.getElem?_eq_getElem hlt' rw [ht'] at this exact (Option.some.inj this).symm rw [List.drop_eq_getElem_cons hlt', hget] split at hp · rename_i _ b1 rw [ok_eq_ok_iff] at hp subst hp cases b1 with | false => have := formula_ok_loop_false terms bound none _ _ _ h exact absurd this (by simp) | true => intro c hc rcases List.mem_cons.mp hc with rfl | hc · exact hr · rw [← hidx] at hc exact ih (terms.length - (index.val + 1)) (by omega) _ (by rw [hidx]) h c hc · rename_i _ e rw [ok_eq_ok_iff] at hp subst hp have := formula_ok_loop_error terms bound _ e _ _ _ h exact absurd this (by simp) · rename_i hge have hle : terms.val.length ≤ index.val := by have : terms.length = terms.val.length := rfl scalar_tac rw [List.drop_eq_nil_of_le hle] simp theorem parts_ok_loop_false (parts : Slice clause_form.Formula) (bound : Slice String) (f : U32) (error : Option first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.parts_ok_loop parts bound f false error index = ok (b, error1)) : b = false := by unfold clause_form.parts_ok_loop at h dsimp only at h split at h · rw [if_neg (by simp)] at h rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.1.symm · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.1.symm theorem parts_ok_loop_error (parts : Slice clause_form.Formula) (bound : Slice String) (f : U32) (ok1 : Bool) (e : first_order.Malformed) (index : Usize) (b : Bool) (error1 : Option first_order.Malformed) (h : clause_form.parts_ok_loop parts bound f ok1 (some e) index = ok (b, error1)) : error1 = some e := by unfold clause_form.parts_ok_loop at h dsimp only at h split at h · split at h · rw [if_neg (by simp)] at h rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.2.symm · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.2.symm · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h exact h.2.symm theorem parts_ok_loop_all (parts : Slice clause_form.Formula) (bound : Slice String) (f : U32) : ∀ (k : Nat) (index : Usize), parts.length - index.val = k → clause_form.parts_ok_loop parts bound f true none index = ok (true, none) → ∀ g ∈ parts.val.drop index.val, clause_form.formula_ok g bound f = ok (.Ok true) := by intro k induction k using Nat.strong_induction_on with | _ k ih => intro index hk h unfold clause_form.parts_ok_loop at h dsimp only at h split at h · rename_i hlt rw [if_pos rfl] at h rw [if_pos (show core.option.Option.is_none (none : Option first_order.Malformed) = true from rfl)] at h read_ok at h obtain ⟨g, hg, r, hr, p, hp, h⟩ := h have hg' := slice_index_usize_eq_ok _ _ _ hg have hlen : parts.length = parts.val.length := rfl have hlt' : index.val < parts.val.length := by have := Slice.len_val parts scalar_tac have hidx : (core.num.Usize.wrapping_add index 1#usize).val = index.val + 1 := usize_succ_val index parts.length hlt' parts.property have hget : parts.val[index.val] = g := by have := List.getElem?_eq_getElem hlt' rw [hg'] at this exact (Option.some.inj this).symm rw [List.drop_eq_getElem_cons hlt', hget] split at hp · rename_i _ b1 rw [ok_eq_ok_iff] at hp subst hp cases b1 with | false => have := parts_ok_loop_false parts bound f none _ _ _ h exact absurd this (by simp) | true => intro c hc rcases List.mem_cons.mp hc with rfl | hc · exact hr · rw [← hidx] at hc exact ih (parts.length - (index.val + 1)) (by omega) _ (by rw [hidx]) h c hc · rename_i _ e rw [ok_eq_ok_iff] at hp subst hp have := parts_ok_loop_error parts bound f _ e _ _ _ h exact absurd this (by simp) · rename_i hge have hle : parts.val.length ≤ index.val := by have := Slice.len_val parts scalar_tac rw [List.drop_eq_nil_of_le hle] simp theorem parts_ok_spec (parts : Slice clause_form.Formula) (bound : Slice String) (f : U32) (h : clause_form.parts_ok parts bound f = ok (.Ok true)) : ∀ g ∈ parts.val, clause_form.formula_ok g bound f = ok (.Ok true) := by unfold clause_form.parts_ok at h read_ok at h obtain ⟨p, hp, h⟩ := h obtain ⟨ok1, error⟩ := p cases error with | some e => simp at h | none => dsimp only at h rw [ok_eq_ok_iff] at h have hok : ok1 = true := by injection h with h try exact h.symm subst hok exact parts_ok_loop_all parts bound f _ 0#usize rfl hp /-- A formula whose body passes under `bound ++ [x]` with `x` new is scoped, closed and clean under `bound` as `all x` and as `exists x`. ```lean theorem formulaOk_binder (x : String) (bound : List String) (body : Sheaf.Formula Value Value) (hx : x ∉ bound) (hb : FormulaOk (bound ++ [x]) body) : FormulaOk bound (.all x body) ∧ FormulaOk bound (.exists x body) ``` #### `binder_ok_spec` `binder_ok`: the variable is new, and the body passes with it bound. ```lean theorem binder_ok_spec (x : String) (s : Str) (hs : strOf x = ok s) (body : clause_form.Formula) (bound : Slice String) (f : U32) (ih : ∀ (bound' : Slice String), clause_form.formula_ok body bound' f = ok (.Ok true) → FormulaOk bound'.val (formulaToSpec body)) (h : clause_form.binder_ok s body bound f = ok (.Ok true)) : x ∉ bound.val ∧ FormulaOk (bound.val ++ [x]) (formulaToSpec body) ``` #### `formula_ok_spec` **`formula_ok` establishes the soundness theorem's hypotheses.** ```lean theorem formula_ok_spec : ∀ (n : Nat) (φ : clause_form.Formula) (bound : Slice String) (f : U32), f.val = n → clause_form.formula_ok φ bound f = ok (.Ok true) → FormulaOk bound.val (formulaToSpec φ) ``` ### `SheafKernel/Skolemizing.lean` **The kernel's Skolemizing walk computes the specification's** `Skolemizer::nnf` is the pure `Sheaf.nnf` (`Sheaf/ClauseForm.lean`) read through `nnfToSpec`, with the sorted map standing for the association list (`EnvRel`) and the kernel's `Skolemizer` for the generator `Sk`. The invariant `WalkInv` carries what the proof needs along every path of the walk: the environment's values mention only universals, no universal is bound in the environment, and the formula's binders avoid both. #### `from_residual_is_err` The generator a kernel `Skolemizer` stands for: its namespace, the kernel's separator, and its counter. -/ def skOf (self : clause_form.Skolemizer) : Sheaf.Sk := ⟨self.namespace, ":", self.counter.val⟩ /-! ## Residuals and clones ```lean theorem from_residual_is_err {T E E' : Type} (inst : core.convert.From E E') (residual : core.result.Result Never E') (rr : core.result.Result T E) (h : core.result.Result.Insts.CoreOpsTry_traitFromResidualResult.from_residual T inst residual = ok rr) : ∃ e, rr = .Err e ``` #### `cf_clone_terms_loop_eq` ```lean theorem cf_clone_terms_loop_eq (items : Slice KTerm) : ∀ (k : Nat) (out out' : alloc.vec.Vec KTerm) (index : Usize), items.length - index.val = k → clause_form.clone_terms_loop items out index = ok out' → out'.val = out.val ++ items.val.drop index.val ``` #### `cf_clone_terms_eq` ```lean theorem cf_clone_terms_eq (items : Slice KTerm) (v : alloc.vec.Vec KTerm) (h : clause_form.clone_terms items = ok v) : v.val = items.val ``` #### `clone_formulas_loop_eq` ```lean theorem clone_formulas_loop_eq (parts : Slice clause_form.Formula) (ih : ∀ g ∈ parts.val, ∀ g', clause_form.Formula.Insts.CoreCloneClone.clone g = ok g' → g' = g) : ∀ (k : Nat) (out out' : alloc.vec.Vec clause_form.Formula) (index : Usize), parts.length - index.val = k → clause_form.clone_formulas_loop parts out index = ok out' → out'.val = out.val ++ parts.val.drop index.val ``` #### `formula_clone_eq` The kernel's `Clone` for formulas is the identity. ```lean theorem formula_clone_eq : ∀ (n : Nat) (φ φ' : clause_form.Formula), sizeOf φ = n → clause_form.Formula.Insts.CoreCloneClone.clone φ = ok φ' → φ' = φ ``` #### `slice_to_vec_terms` ```lean theorem slice_to_vec_terms (U : Slice KTerm) (v : alloc.vec.Vec KTerm) (h : alloc.slice.Slice.to_vec first_order.Term.Insts.CoreCloneClone U = ok v) : v.val = U.val ``` #### `string_from_strOf` ```lean theorem string_from_strOf (x : String) (s : Str) (hs : strOf x = ok s) (u : String) (h : alloc.string.String.Insts.CoreConvertFromShared0Str.from s = ok u) : u = x ``` #### `witness_spec` `Skolemizer::witness` builds the spec's witness term for the generator's next name, and advances the generator. ```lean theorem witness_spec (self : clause_form.Skolemizer) (U : Slice KTerm) (w : KTerm) (self' : clause_form.Skolemizer) (h : clause_form.Skolemizer.witness self U = ok (.Ok w, self')) : termToSpec w = Sheaf.witness (skOf self).name (U.val.map termToSpec) ∧ skOf self' = (skOf self).next ``` #### `WalkInv.universal_of` What holds of the environment, the universals and the formula along every path of the walk. -/ structure WalkInv (σ : KEnv) (E : Sheaf.Env Value) (U : Slice KTerm) (φ : Sheaf.Formula Value Value) : Prop where rel : EnvRel σ E uvars : ∀ u ∈ U.val, (termToSpec u).isVar uFree : ∀ u ∈ U.val, ∀ y ∈ (termToSpec u).vars, ¬ IsKey σ y vals : ∀ e ∈ σ.entries.val, ∀ y ∈ (termToSpec e.2).vars, ∃ u ∈ U.val, y ∈ (termToSpec u).vars binders : φ.Scoped (fun y => IsKey σ y ∨ ∃ u ∈ U.val, y ∈ (termToSpec u).vars) theorem WalkInv.valsFree {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {φ : Sheaf.Formula Value Value} (h : WalkInv σ E U φ) : ValsFree σ := by intro e he y hy obtain ⟨u, hu, hyu⟩ := h.vals e he y hy exact h.uFree u hu y hyu theorem WalkInv.scoped {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {φ ψ : Sheaf.Formula Value Value} (h : WalkInv σ E U φ) (hψ : ψ.Scoped (fun y => IsKey σ y ∨ ∃ u ∈ U.val, y ∈ (termToSpec u).vars)) : WalkInv σ E U ψ := ⟨h.rel, h.uvars, h.uFree, h.vals, hψ⟩ theorem WalkInv.not {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {f : Sheaf.Formula Value Value} (h : WalkInv σ E U (.not f)) : WalkInv σ E U f := by apply h.scoped have := h.binders rw [Sheaf.Formula.Scoped] at this exact this theorem WalkInv.and_part {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {parts : List (Sheaf.Formula Value Value)} (h : WalkInv σ E U (.and parts)) : ∀ f ∈ parts, WalkInv σ E U f := by intro f hf apply h.scoped have := h.binders rw [Sheaf.Formula.Scoped] at this exact this ⟨f, hf⟩ (List.mem_attach _ _) theorem WalkInv.or_part {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {parts : List (Sheaf.Formula Value Value)} (h : WalkInv σ E U (.or parts)) : ∀ f ∈ parts, WalkInv σ E U f := by intro f hf apply h.scoped have := h.binders rw [Sheaf.Formula.Scoped] at this exact this ⟨f, hf⟩ (List.mem_attach _ _) theorem WalkInv.implies_or {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {a c : Sheaf.Formula Value Value} (h : WalkInv σ E U (.implies a c)) : WalkInv σ E U (.or [.not a, c]) := by apply h.scoped have := h.binders rw [Sheaf.Formula.Scoped] at this rw [Sheaf.Formula.Scoped] intro f _ have hf := f.property simp only [List.mem_cons, List.not_mem_nil, or_false] at hf rcases hf with hf | hf · rw [hf, Sheaf.Formula.Scoped] exact this.1 · rw [hf] exact this.2 /-- Entering a universal: the variable joins the universals. ```lean theorem WalkInv.universal_of {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {φ : Sheaf.Formula Value Value} (h : WalkInv σ E U φ) (x : String) (body : Sheaf.Formula Value Value) (hx : ¬ (IsKey σ x ∨ ∃ u ∈ U.val, x ∈ (termToSpec u).vars)) (hb : body.Scoped (fun y => y = x ∨ (IsKey σ y ∨ ∃ u ∈ U.val, y ∈ (termToSpec u).vars))) (U' : Slice KTerm) (hU' : U'.val = U.val ++ [.Var x]) : WalkInv σ E U' body ``` #### `WalkInv.skolem_of` Entering an existential: the variable is bound to a witness over the universals. ```lean theorem WalkInv.skolem_of {σ : KEnv} {E : Sheaf.Env Value} {U : Slice KTerm} {φ : Sheaf.Formula Value Value} (h : WalkInv σ E U φ) (x : String) (body : Sheaf.Formula Value Value) (hx : ¬ (IsKey σ x ∨ ∃ u ∈ U.val, x ∈ (termToSpec u).vars)) (hb : body.Scoped (fun y => y = x ∨ (IsKey σ y ∨ ∃ u ∈ U.val, y ∈ (termToSpec u).vars))) (σ' : KEnv) (w : KTerm) (hw : ∀ y ∈ (termToSpec w).vars, ∃ u ∈ U.val, y ∈ (termToSpec u).vars) (hins : ∀ e, e ∈ σ'.entries.val ↔ e = (x, w) ∨ e ∈ σ.entries.val) : WalkInv σ' ((x, termToSpec w) :: E) U body ``` #### `nnf_list_loop_error` ```lean theorem nnf_list_loop_error (parts : Slice clause_form.Formula) (neg : Bool) (σ : KEnv) (U : Slice KTerm) (f : U32) (self : clause_form.Skolemizer) (out : alloc.vec.Vec clause_form.Nnf) (e : clause_form.CnfError) (index : Usize) (res : clause_form.Skolemizer × alloc.vec.Vec clause_form.Nnf × Option clause_form.CnfError) (h : clause_form.Skolemizer.nnf_list_loop self parts neg σ U f out (some e) index = ok res) : res.2.2 = some e ``` #### `nnf_list_loop_refines` ```lean theorem nnf_list_loop_refines (parts : Slice clause_form.Formula) (neg : Bool) (σ : KEnv) (U : Slice KTerm) (f : U32) (E : Sheaf.Env Value) (ih : ∀ (self : clause_form.Skolemizer) (g : clause_form.Formula) (r : clause_form.Nnf) (self' : clause_form.Skolemizer), g ∈ parts.val → WalkInv σ E U (formulaToSpec g) → clause_form.Skolemizer.nnf self g neg σ U f = ok (.Ok r, self') → nnfToSpec r = (Sheaf.nnf (skOf self) neg E (U.val.map termToSpec) (formulaToSpec g)).1 ∧ skOf self' = (Sheaf.nnf (skOf self) neg E (U.val.map termToSpec) (formulaToSpec g)).2) (hinv : ∀ g ∈ parts.val, WalkInv σ E U (formulaToSpec g)) : ∀ (k : Nat) (self : clause_form.Skolemizer) (out out1 : alloc.vec.Vec clause_form.Nnf) (index : Usize) (self1 : clause_form.Skolemizer), parts.length - index.val = k → clause_form.Skolemizer.nnf_list_loop self parts neg σ U f out none index = ok (self1, out1, none) → out1.val.map nnfToSpec = out.val.map nnfToSpec ++ (Sheaf.nnfList (skOf self) neg E (U.val.map termToSpec) ((parts.val.drop index.val).map formulaToSpec)).1 ∧ skOf self1 = (Sheaf.nnfList (skOf self) neg E (U.val.map termToSpec) ((parts.val.drop index.val).map formulaToSpec)).2 ``` #### `nnf_list_refines` ```lean theorem nnf_list_refines (parts : Slice clause_form.Formula) (neg : Bool) (σ : KEnv) (U : Slice KTerm) (f : U32) (E : Sheaf.Env Value) (ih : ∀ (self : clause_form.Skolemizer) (g : clause_form.Formula) (r : clause_form.Nnf) (self' : clause_form.Skolemizer), g ∈ parts.val → WalkInv σ E U (formulaToSpec g) → clause_form.Skolemizer.nnf self g neg σ U f = ok (.Ok r, self') → nnfToSpec r = (Sheaf.nnf (skOf self) neg E (U.val.map termToSpec) (formulaToSpec g)).1 ∧ skOf self' = (Sheaf.nnf (skOf self) neg E (U.val.map termToSpec) (formulaToSpec g)).2) (hinv : ∀ g ∈ parts.val, WalkInv σ E U (formulaToSpec g)) (self : clause_form.Skolemizer) (out : alloc.vec.Vec clause_form.Nnf) (self1 : clause_form.Skolemizer) (h : clause_form.Skolemizer.nnf_list self parts neg σ U f = ok (.Ok out, self1)) : out.val.map nnfToSpec = (Sheaf.nnfList (skOf self) neg E (U.val.map termToSpec) (parts.val.map formulaToSpec)).1 ∧ skOf self1 = (Sheaf.nnfList (skOf self) neg E (U.val.map termToSpec) (parts.val.map formulaToSpec)).2 ``` #### `first_order_not_spec` ```lean theorem first_order_not_spec (b r : Bool) (h : first_order.not b = ok r) : r = !b ``` #### `nnf_refines` **`Skolemizer::nnf` computes the pure walk.** ```lean theorem nnf_refines : ∀ (n : Nat) (self : clause_form.Skolemizer) (φ : clause_form.Formula) (neg : Bool) (σ : KEnv) (U : Slice KTerm) (f : U32) (r : clause_form.Nnf) (self' : clause_form.Skolemizer) (E : Sheaf.Env Value), f.val = n → WalkInv σ E U (formulaToSpec φ) → clause_form.Skolemizer.nnf self φ neg σ U f = ok (.Ok r, self') → nnfToSpec r = (Sheaf.nnf (skOf self) neg E (U.val.map termToSpec) (formulaToSpec φ)).1 ∧ skOf self' = (Sheaf.nnf (skOf self) neg E (U.val.map termToSpec) (formulaToSpec φ)).2 ``` ### `SheafKernel/Distribution.lean` **Distribution into clauses, and the soundness of `clause_form::clauses`** `cnf` distributes `or` over `and` into sets of literals; the pure `Sheaf.cnf` does the same with lists. The kernel's clauses are sets, so the two agree up to the literals each clause holds: every kernel clause *covers* some pure clause (holds every literal of it), which is all soundness needs, since a clause with more literals is weaker. With `formula_ok_spec`, `nnf_refines` and `clauseForm_sound`, this gives the theorem of this file: wherever the formula handed to `clause_form::clauses` is true, some witness functions for the namespace's names make every clause it returns true. #### `of` ```lean theorem of this file: wherever the formula handed to `clause_form::clauses` is true, some witness functions for the namespace's names make every clause it returns true. -/ namespace SheafKernel open Aeneas Aeneas.Std Result sheaf_kernel /-- Every kernel clause holds every literal of some clause of `ps`. -/ def Covers (ks : List KClause) (ps : List SClause) : Prop ``` #### `cnf_list_loop_error` `c` holds exactly the literals of `p` and of `g`. -/ def Merged (p g c : KClause) : Prop := (∀ l ∈ p.items.val, l ∈ c.items.val) ∧ (∀ l ∈ g.items.val, l ∈ c.items.val) ∧ ∀ l ∈ c.items.val, l ∈ p.items.val ∨ l ∈ g.items.val /-- Every literal of every kernel clause satisfies `Q`. -/ def LitsIn (ks : List KClause) (Q : SLiteral → Prop) : Prop := ∀ c ∈ ks, ∀ l ∈ clauseToSpec c, Q l theorem forall₂_mem_right {α β : Type} {R : α → β → Prop} : ∀ {l1 : List α} {l2 : List β}, List.Forall₂ R l1 l2 → ∀ b ∈ l2, ∃ a ∈ l1, R a b := by intro l1 l2 h induction h with | nil => intro b hb; simp at hb | cons h1 _ ih => intro b hb rcases List.mem_cons.mp hb with rfl | hb · exact ⟨_, List.mem_cons_self, h1⟩ · obtain ⟨a, ha, hab⟩ := ih b hb exact ⟨a, List.mem_cons_of_mem _ ha, hab⟩ theorem forall₂_swap {α β : Type} {R : α → β → Prop} : ∀ {l1 : List α} {l2 : List β}, List.Forall₂ R l1 l2 → List.Forall₂ (fun b a => R a b) l2 l1 := by intro l1 l2 h induction h with | nil => exact List.Forall₂.nil | cons h1 _ ih => exact List.Forall₂.cons h1 ih theorem cnf_lit (l : SLiteral) : Sheaf.cnf (.lit l) = [[l]] := by rw [Sheaf.cnf] /-! ## The groups of a connective ```lean theorem cnf_list_loop_error (parts : Slice clause_form.Nnf) (f : U32) (groups groups1 : alloc.vec.Vec (alloc.vec.Vec KClause)) (e : clause_form.CnfError) (index : Usize) (error1 : Option clause_form.CnfError) (h : clause_form.cnf_list_loop parts f groups (some e) index = ok (groups1, error1)) : error1 = some e ``` #### `cnf_list_loop_rel` ```lean theorem cnf_list_loop_rel (parts : Slice clause_form.Nnf) (f : U32) : ∀ (k : Nat) (groups groups1 : alloc.vec.Vec (alloc.vec.Vec KClause)) (index : Usize), parts.length - index.val = k → clause_form.cnf_list_loop parts f groups none index = ok (groups1, none) → ∃ gs, groups1.val = groups.val ++ gs ∧ List.Forall₂ (fun n g => clause_form.cnf n f = ok (.Ok g)) (parts.val.drop index.val) gs ``` #### `cnf_list_rel` ```lean theorem cnf_list_rel (parts : Slice clause_form.Nnf) (f : U32) (groups : alloc.vec.Vec (alloc.vec.Vec KClause)) (h : clause_form.cnf_list parts f = ok (.Ok groups)) : List.Forall₂ (fun n g => clause_form.cnf n f = ok (.Ok g)) parts.val groups.val ``` #### `flatten_inner` ```lean theorem flatten_inner (group : alloc.vec.Vec KClause) : ∀ (k : Nat) (result result1 : alloc.vec.Vec KClause) (inner : Usize), group.length - inner.val = k → clause_form.flatten_groups_loop0_loop0 result group inner = ok result1 → result1.val = result.val ++ group.val.drop inner.val ``` #### `flatten_outer` ```lean theorem flatten_outer (groups : Slice (alloc.vec.Vec KClause)) : ∀ (k : Nat) (result r : alloc.vec.Vec KClause) (index : Usize), groups.length - index.val = k → clause_form.flatten_groups_loop0 groups result index = ok r → r.val = result.val ++ (groups.val.drop index.val).flatMap (fun g => g.val) ``` #### `flatten_groups_spec` ```lean theorem flatten_groups_spec (groups : Slice (alloc.vec.Vec KClause)) (r : alloc.vec.Vec KClause) (h : clause_form.flatten_groups groups = ok r) : r.val = groups.val.flatMap (fun g => g.val) ``` #### `extend_from_loop_mem` ```lean theorem extend_from_loop_mem (self other : KClause) : ∀ (k : Nat) (s : KClause) (index : Usize) (s' : KClause), other.items.length - index.val = k → sorted_collections.Set.extend_from_loop first_order.Literal.Insts.CoreCmpOrd first_order.Literal.Insts.CoreCloneClone s other index = ok s' → (∀ y ∈ s.items.val, y ∈ s'.items.val) ∧ ∀ y ∈ other.items.val.drop index.val, y ∈ s'.items.val ``` #### `extend_from_mem` ```lean theorem extend_from_mem (s other s' : KClause) (h : sorted_collections.Set.extend_from first_order.Literal.Insts.CoreCmpOrd first_order.Literal.Insts.CoreCloneClone s other = ok s') : (∀ y ∈ s.items.val, y ∈ s'.items.val) ∧ ∀ y ∈ other.items.val, y ∈ s'.items.val ``` #### `set_insert_subset` `insert` adds nothing but the item. ```lean theorem set_insert_subset {T : Type} (inst : core.cmp.Ord T) (s : sorted_collections.Set T) (item : T) (b : Bool) (s' : sorted_collections.Set T) (h : sorted_collections.Set.insert inst s item = ok (b, s')) : ∀ y ∈ s'.items.val, y ∈ s.items.val ∨ y = item ``` #### `extend_from_loop_subset` ```lean theorem extend_from_loop_subset (other : KClause) : ∀ (k : Nat) (s : KClause) (index : Usize) (s' : KClause), other.items.length - index.val = k → sorted_collections.Set.extend_from_loop first_order.Literal.Insts.CoreCmpOrd first_order.Literal.Insts.CoreCloneClone s other index = ok s' → ∀ y ∈ s'.items.val, y ∈ s.items.val ∨ y ∈ other.items.val ``` #### `extend_from_subset` ```lean theorem extend_from_subset (s other s' : KClause) (h : sorted_collections.Set.extend_from first_order.Literal.Insts.CoreCmpOrd first_order.Literal.Insts.CoreCloneClone s other = ok s') : ∀ y ∈ s'.items.val, y ∈ s.items.val ∨ y ∈ other.items.val ``` #### `distribute_inner` ```lean theorem distribute_inner (partials group : Slice KClause) (pi : Usize) : ∀ (k : Nat) (next next1 : alloc.vec.Vec KClause) (ci : Usize), group.length - ci.val = k → clause_form.distribute_loop0_loop0 partials group next pi ci = ok next1 → ∀ c ∈ next1.val, c ∈ next.val ∨ ∃ p ∈ partials.val, ∃ g ∈ group.val, Merged p g c ``` #### `distribute_outer` ```lean theorem distribute_outer (partials group : Slice KClause) : ∀ (k : Nat) (next next1 : alloc.vec.Vec KClause) (pi : Usize), partials.length - pi.val = k → clause_form.distribute_loop0 partials group next pi = ok next1 → ∀ c ∈ next1.val, c ∈ next.val ∨ ∃ p ∈ partials.val, ∃ g ∈ group.val, Merged p g c ``` #### `distribute_covers` A distribution step covers the pure distribution. ```lean theorem distribute_covers (partials group : Slice KClause) (next : alloc.vec.Vec KClause) (h : clause_form.distribute partials group = ok next) (P G : List SClause) (hP : Covers partials.val P) (hG : Covers group.val G) : Covers next.val (Sheaf.distribute P G) ``` #### `cnf_loop_covers` ```lean theorem cnf_loop_covers (groups : alloc.vec.Vec (alloc.vec.Vec KClause)) : ∀ (k : Nat) (result result2 : alloc.vec.Vec KClause) (gi : Usize) (Ps : List (List SClause)) (acc : List SClause), groups.length - gi.val = k → List.Forall₂ (fun (g : alloc.vec.Vec KClause) P => Covers g.val P) (groups.val.drop gi.val) Ps → Covers result.val acc → clause_form.cnf_loop groups result gi = ok result2 → Covers result2.val (Ps.foldl Sheaf.distribute acc) ``` #### `distribute_lits_in` ```lean theorem distribute_lits_in (partials group : Slice KClause) (next : alloc.vec.Vec KClause) (h : clause_form.distribute partials group = ok next) (Q : SLiteral → Prop) (hP : LitsIn partials.val Q) (hG : LitsIn group.val Q) : LitsIn next.val Q ``` #### `cnf_loop_lits_in` ```lean theorem cnf_loop_lits_in (groups : alloc.vec.Vec (alloc.vec.Vec KClause)) (Q : SLiteral → Prop) : ∀ (k : Nat) (result result2 : alloc.vec.Vec KClause) (gi : Usize), groups.length - gi.val = k → (∀ g ∈ groups.val.drop gi.val, LitsIn g.val Q) → LitsIn result.val Q → clause_form.cnf_loop groups result gi = ok result2 → LitsIn result2.val Q ``` #### `cnf_refines` ```lean theorem cnf_refines : ∀ (n : Nat) (nnf : clause_form.Nnf) (f : U32) (cs : alloc.vec.Vec KClause), f.val = n → clause_form.cnf nnf f = ok (.Ok cs) → Covers cs.val (Sheaf.cnf (nnfToSpec nnf)) ``` #### `cnf_lits_in` Every literal of every clause `cnf` returns is a literal of the normal form. ```lean theorem cnf_lits_in : ∀ (n : Nat) (nnf : clause_form.Nnf) (f : U32) (cs : alloc.vec.Vec KClause), f.val = n → clause_form.cnf nnf f = ok (.Ok cs) → LitsIn cs.val (· ∈ (nnfToSpec nnf).lits) ``` #### `has_byte_loop_spec` ```lean theorem has_byte_loop_spec (bytes : Slice U8) (w : U8) : ∀ (k : Nat) (found : Bool) (index : Usize) (b : Bool), bytes.length - index.val = k → first_order.has_byte_loop bytes w found index = ok b → (b = true ↔ found = true ∨ w ∈ bytes.val.drop index.val) ``` #### `has_byte_spec` ```lean theorem has_byte_spec (bytes : Slice U8) (w : U8) (b : Bool) (h : first_order.has_byte bytes w = ok b) : b = true ↔ w ∈ bytes.val ``` #### `clauses_walk` What `clause_form::clauses` computes: the namespace decodes and carries no separator, the formula passes `formula_ok` under no bound variables, and the clauses are the distribution of the kernel's normal form, which is the pure walk's. ```lean theorem clauses_walk (φ : clause_form.Formula) (ns : Str) (cs : alloc.vec.Vec KClause) (h : clause_form.clauses φ ns = ok (.Ok cs)) : ∃ (nsS : String) (val1 : clause_form.Nnf), decodeUtf8 ns.val = some nsS ∧ (58#u8) ∉ ns.val ∧ FormulaOk [] (formulaToSpec φ) ∧ nnfToSpec val1 = (Sheaf.nnf ⟨nsS, ":", 0⟩ false [] [] (formulaToSpec φ)).1 ∧ clause_form.cnf val1 clause_form.FORMULA_FUEL = ok (.Ok cs) ``` #### `FormulaOk.closed` A formula that passes `formula_ok` under no bound variables is closed. ```lean theorem FormulaOk.closed {φ : Sheaf.Formula Value Value} (hok : FormulaOk [] φ) : φ.FV = [] ``` #### `FormulaOk.scopedFalse` ```lean theorem FormulaOk.scopedFalse {φ : Sheaf.Formula Value Value} (hok : FormulaOk [] φ) : φ.Scoped (fun _ => False) ``` #### `FormulaOk.noNames` ```lean theorem FormulaOk.noNames {φ : Sheaf.Formula Value Value} (hok : FormulaOk [] φ) : φ.names = [] ``` #### `clauses_sound` **Soundness of `clause_form::clauses`.** Wherever the formula is true, some witness functions for the namespace's Skolem names make every returned clause true. ```lean theorem clauses_sound (φ : clause_form.Formula) (ns : Str) (cs : alloc.vec.Vec KClause) (h : clause_form.clauses φ ns = ok (.Ok cs)) (M : Sheaf.Structure Value Value) (hφ : (formulaToSpec φ).true M) : ∃ (nsS : String) (fs : String → Option (List M.D → M.D)), decodeUtf8 ns.val = some nsS ∧ (58#u8) ∉ ns.val ∧ (∀ s, fs s ≠ none → (Sheaf.Sk.mk nsS ":" 0).Fresh s) ∧ ∀ c ∈ cs.val, (clauseToSpec c).true (M.withSkolems fs) ``` #### `clauses_names` **The names of the clauses are the namespace's.** Every Skolem name in a clause `clause_form::clauses` returns was issued in its namespace. ```lean theorem clauses_names (φ : clause_form.Formula) (ns : Str) (cs : alloc.vec.Vec KClause) (h : clause_form.clauses φ ns = ok (.Ok cs)) : ∃ nsS : String, decodeUtf8 ns.val = some nsS ∧ (58#u8) ∉ ns.val ∧ ∀ c ∈ cs.val, ∀ l ∈ clauseToSpec c, ∀ s ∈ l.names, (Sheaf.Sk.mk nsS ":" 0).Fresh s ``` ### `SheafKernel/Namespaces.lean` **Namespaces and the names they issue** A Skolem name is `:`. When no namespace contains `:` (which `clause_form::clauses` refuses), a name determines its namespace: two namespaces that both issued a name are the same string. This is what lets one set of witness functions serve every premise and the goal of a certificate at once. #### `digitChar_ne_colon` ```lean theorem digitChar_ne_colon (d : Nat) (hd : d < 10) : Nat.digitChar d ≠ ':' ``` #### `toDigits_ten_ne_colon` ```lean theorem toDigits_ten_ne_colon : ∀ (n : Nat), ∀ c ∈ Nat.toDigits 10 n, c ≠ ':' ``` #### `repr_toList` ```lean theorem repr_toList (n : Nat) : (Nat.repr n).toList = Nat.toDigits 10 n ``` #### `append_colon_inj` Two decompositions at a character absent from both prefixes agree on the prefixes. ```lean theorem append_colon_inj : ∀ (l1 l2 d1 d2 : List Char), l1 ++ ':' :: d1 = l2 ++ ':' :: d2 → ':' ∉ l1 → ':' ∉ l2 → l1 = l2 | [], [], _, _, _, _, _ => rfl | [], c :: l2, d1, d2, h, _, h2 => by simp only [List.nil_append, List.cons_append, List.cons.injEq] at h obtain ⟨hc, _⟩ ``` #### `fresh_unique` A name issued in one namespace is issued in no other, when namespaces carry no `:`. ```lean theorem fresh_unique (ns1 ns2 : String) (h1 : ':' ∉ ns1.toList) (h2 : ':' ∉ ns2.toList) (s : String) (f1 : (Sheaf.Sk.mk ns1 ":" 0).Fresh s) (f2 : (Sheaf.Sk.mk ns2 ":" 0).Fresh s) : ns1 = ns2 ``` #### `colon_byte_of_mem` A `:` among a string's characters is a `58` among its UTF-8 bytes. ```lean theorem colon_byte_of_mem (ns : String) (h : ':' ∈ ns.toList) : (58 : UInt8) ∈ ns.toUTF8.data.toList ``` #### `no_colon_of_bytes` The kernel's byte check on a namespace, read on the decoded string. ```lean theorem no_colon_of_bytes (ns : Str) (nsS : String) (hdec : decodeUtf8 ns.val = some nsS) (hno : (58#u8) ∉ ns.val) : ':' ∉ nsS.toList ``` ### `SheafKernel/Leaves.lean` **The leaves of a certificate are translations** `check_tree` recomputes a tree's hash, retranslates the tree in its namespace and compares the declared clause set with the computed one; `load_clauses` then registers the declared clauses as leaves. So every leaf a premise or the goal contributes is a clause `translate_clauses` computed for its tree, which `clauses_sound` and `clauses_names` describe. #### `clause_cmp_eq` The kernel's order on clauses says `Equal` only for equal clauses. ```lean theorem clause_cmp_eq (a b : KClause) (h : sorted_collections.Set.Insts.CoreCmpOrd.cmp first_order.Literal.Insts.CoreCmpOrd a b = ok Ordering.eq) : a = b ``` #### `clause_eq_eq` The kernel's equality on clauses says `true` only for equal clauses. ```lean theorem clause_eq_eq (a b : KClause) (h : sorted_collections.Set.Insts.CoreCmpPartialEqSet.eq first_order.Literal.Insts.CoreCmpPartialEqLiteral a b = ok true) : a = b ``` #### `clause_set_ne_false` Two clause sets the kernel does not find different are equal. ```lean theorem clause_set_ne_false (a b : sorted_collections.Set KClause) (h : core.cmp.PartialEq.ne.trait_default (sorted_collections.Set.Insts.CoreCmpPartialEqSet (sorted_collections.Set.Insts.CoreCmpPartialEqSet first_order.Literal.Insts.CoreCmpPartialEqLiteral)) a b = ok false) : a = b ``` #### `clause_set_loop_subset` ```lean theorem clause_set_loop_subset (clauses : Slice KClause) : ∀ (k : Nat) (out out' : sorted_collections.Set KClause) (index : Usize), clauses.length - index.val = k → certificate_check.clause_set_loop clauses out index = ok out' → ∀ c ∈ out'.items.val, c ∈ out.items.val ∨ c ∈ clauses.val ``` #### `clause_set_subset` ```lean theorem clause_set_subset (clauses : Slice KClause) (set : sorted_collections.Set KClause) (h : certificate_check.clause_set clauses = ok set) : ∀ c ∈ set.items.val, c ∈ clauses.val ``` #### `declared_clauses_loop_malformed` ```lean theorem declared_clauses_loop_malformed (list : Slice Value) (declared declared1 : sorted_collections.Set KClause) (index : Usize) (m : Bool) (h : certificate_check.declared_clauses_loop list declared true index = ok (declared1, m)) : m = true ``` #### `declared_clauses_loop_mem` ```lean theorem declared_clauses_loop_mem (list : Slice Value) : ∀ (k : Nat) (declared declared1 : sorted_collections.Set KClause) (index : Usize), list.length - index.val = k → certificate_check.declared_clauses_loop list declared false index = ok (declared1, false) → (∀ c ∈ declared.items.val, c ∈ declared1.items.val) ∧ ∀ v ∈ list.val.drop index.val, ∀ c, first_order.clause_from_value v = ok (.Ok c) → c ∈ declared1.items.val ``` #### `declared_clauses_mem` ```lean theorem declared_clauses_mem (list : Slice Value) (declared : sorted_collections.Set KClause) (h : certificate_check.declared_clauses list = ok (some declared)) : ∀ v ∈ list.val, ∀ c, first_order.clause_from_value v = ok (.Ok c) → c ∈ declared.items.val ``` #### `well_formed_clause_from_value_some` ```lean theorem well_formed_clause_from_value_some (v : Value) (c : KClause) (h : certificate_check.well_formed_clause_from_value v = ok (some c)) : first_order.clause_from_value v = ok (.Ok c) ``` #### `load_clauses_loop_failure` ```lean theorem load_clauses_loop_failure (id : Str) (into into1 : KMap) (list : alloc.vec.Vec Value) (e : certificate_check.Verdict) (index : Usize) (f : Option certificate_check.Verdict) (h : certificate_check.load_clauses_loop id into list (some e) index = ok (into1, f)) : f = some e ``` #### `load_clauses_loop_values` ```lean theorem load_clauses_loop_values (id : Str) (list : alloc.vec.Vec Value) : ∀ (k : Nat) (into into1 : KMap) (index : Usize), list.length - index.val = k → certificate_check.load_clauses_loop id into list none index = ok (into1, none) → ∀ c ∈ values into1, c ∈ values into ∨ ∃ v ∈ list.val.drop index.val, first_order.clause_from_value v = ok (.Ok c) ``` #### `list_field_spec` ```lean theorem list_field_spec (v : Value) (key what : Str) (l : alloc.vec.Vec Value) (h : certificate_check.list_field v key what = ok (.Ok l)) : ∃ items : alloc.vec.Vec Value, certificate_check.field v key = ok (.Ok (.List items)) ∧ l = items ``` #### `load_clauses_values` The leaves `load_clauses` adds are clauses declared in the owner's `clauses` list. ```lean theorem load_clauses_values (owner : Value) (id : Str) (into into' : KMap) (h : certificate_check.load_clauses owner id into = ok (.Ok (), into')) : ∃ items : alloc.vec.Vec Value, certificate_check.field owner (toStr "clauses") = ok (.Ok (.List items)) ∧ ∀ c ∈ values into', c ∈ values into ∨ ∃ v ∈ items.val, first_order.clause_from_value v = ok (.Ok c) ``` #### `translate_clauses_spec` ```lean theorem translate_clauses_spec (tree : schema_tree.Tree) (profile : working_graph.Profile) (ns sk : Str) (negated : Bool) (cs : alloc.vec.Vec KClause) (h : translation.translate_clauses tree profile ns sk negated = ok (.Ok cs)) : ∃ φ : clause_form.Formula, translation.translate tree profile ns = ok (.Ok φ) ∧ clause_form.clauses (if negated then .Not φ else φ) sk = ok (.Ok cs) ``` #### `check_tree_spec` **`check_tree`**: the owner's tree translates in the namespace, and every clause declared under it is one of the computed clauses. ```lean theorem check_tree_spec (owner : Value) (id declared_hash : Str) (profile : working_graph.Profile) (ns sk : Str) (negated : Bool) (h : certificate_check.check_tree owner id declared_hash profile ns sk negated = ok (.Ok ())) : ∃ (treeV : Value) (tree : schema_tree.Tree) (cs : alloc.vec.Vec KClause) (items : alloc.vec.Vec Value), certificate_check.field owner (toStr "tree") = ok (.Ok treeV) ∧ schema_tree.Tree.from_value treeV = ok (.Ok tree) ∧ translation.translate_clauses tree profile ns sk negated = ok (.Ok cs) ∧ certificate_check.field owner (toStr "clauses") = ok (.Ok (.List items)) ∧ ∀ v ∈ items.val, ∀ c, first_order.clause_from_value v = ok (.Ok c) → c ∈ cs.val ``` ### `SheafKernel/Combine.lean` **One set of witness functions for every namespace** `clauses_sound` gives, for one formula in one namespace, witness functions for that namespace's names. A certificate has several premises and a goal, each translated in its own namespace. Since no namespace contains `:` and a name determines its namespace (`fresh_unique`), the per-namespace witness functions combine into one that makes every group's clauses true at once, provided groups that share a namespace share their clauses (which the hash discipline gives: the same namespace means the same hash, so the same tree and the same clauses). #### `combine_groups` A premise's or the goal's contribution: the namespace its Skolem names are issued in (as the kernel saw it and as a string), the formula whose clause form it declares, the clauses of that clause form, and, for the hash discipline, the tree's declared hash and the translator's output before any negation. -/ structure Group where ns : Str nsS : String φ : clause_form.Formula cs : alloc.vec.Vec KClause hash : String base : clause_form.Formula /-- The names of a group's clauses are issued in its namespace. -/ def Group.NamesOwn (g : Group) : Prop := ∀ c ∈ g.cs.val, ∀ l ∈ clauseToSpec c, ∀ s ∈ l.names, (Sheaf.Sk.mk g.nsS ":" 0).Fresh s /-- The group's namespace decodes and carries no separator. -/ def Group.NsOk (g : Group) : Prop := decodeUtf8 g.ns.val = some g.nsS ∧ (58#u8) ∉ g.ns.val /-- Some witness functions for the group's namespace make all its clauses true in `M`. -/ def Group.Holds (g : Group) (M : Sheaf.Structure Value Value) : Prop := ∃ fs : String → Option (List M.D → M.D), (∀ s, fs s ≠ none → (Sheaf.Sk.mk g.nsS ":" 0).Fresh s) ∧ ∀ c ∈ g.cs.val, (clauseToSpec c).true (M.withSkolems fs) theorem find?_congr {α : Type} (p q : α → Bool) : ∀ (l : List α), (∀ x ∈ l, p x = q x) → l.find? p = l.find? q := by intro l induction l with | nil => intro _; rfl | cons x rest ih => intro h rw [List.find?_cons, List.find?_cons, h x List.mem_cons_self] split · rfl · exact ih (fun y hy => h y (List.mem_cons_of_mem _ hy)) /-- **Combining witness functions.** When every group's names are its own, its namespace is clean, groups sharing a namespace share their clauses, and each group holds on its own, one set of witness functions makes every group hold. ```lean theorem combine_groups (M : Sheaf.Structure Value Value) (groups : List Group) (hns : ∀ g ∈ groups, g.NsOk) (hnames : ∀ g ∈ groups, g.NamesOwn) (hshare : ∀ g1 ∈ groups, ∀ g2 ∈ groups, g1.nsS = g2.nsS → g1.cs = g2.cs) (hholds : ∀ g ∈ groups, g.Holds M) : ∃ fs : String → Option (List M.D → M.D), ∀ g ∈ groups, ∀ c ∈ g.cs.val, (clauseToSpec c).true (M.withSkolems fs) ``` ### `SheafKernel/Certificate.lean` **What an accepted certificate says** `check_inner_sound` (Certificates.lean) shows that an accepted certificate's leaf clauses are unsatisfiable, unless an `identity` step was accepted against the goal's hash. Here the leaves are read as what they are: the clause forms of the premises' trees, each translated in its hash's namespace, and of the goal's tree, translated in its own hash's namespace and negated for a proof. With `clauses_sound` for each group and `combine_groups` across namespaces, an accepted certificate means that the premise formulas, together with the goal's clause-form formula, have no model: a proof entails the goal, a disproof refutes it. An `identity` step is sound for the same reason as the rest: it names a premise with the goal's hash, so (by the hash discipline) the premise's formula is the goal's, which a proof negates. The one assumption left explicit is the hash discipline, `Consistent`: two groups in the same namespace translate to the same formula, and two groups with the same hash have the same tree, so the same translation. The kernel checks each declared hash against its own hash of the tree, so this is the collision freedom of that hash on the trees in the certificate. #### `push_str_spec` ```lean theorem push_str_spec (t : String) (x : Str) (r : String) (h : alloc.string.String.push_str t x = ok r) : ∃ s, decodeUtf8 x.val = some s ∧ r = t ++ s ``` #### `concat_spec` ```lean theorem concat_spec (a b : Str) (r : String) (h : first_order.concat a b = ok r) : ∃ sa sb, decodeUtf8 a.val = some sa ∧ decodeUtf8 b.val = some sb ∧ r = sa ++ sb ``` #### `namespace_of_spec` A premise's namespace begins with `@`. ```lean theorem namespace_of_spec (hash : Str) (s : String) (h : certificate_check.namespace_of hash = ok s) : ∃ rest, s = "@" ++ rest ``` #### `at_ne_target` ```lean theorem at_ne_target (rest : String) : "@" ++ rest ≠ "target" ``` #### `text_spec` ```lean theorem text_spec (v : Value) (key : Str) (s : String) (h : certificate_check.text v key = ok (.Ok s)) : certificate_check.field v key = ok (.Ok (.Text s)) ``` #### `strOf_empty_val` `g` is what the kernel computed for the premise value `p`: its hash names the namespace, its tree translates there, and its clauses are the clause form. -/ def PremiseOf (p : Value) (profile : working_graph.Profile) (g : Group) : Prop := ∃ (hashS : Str) (treeV : Value) (tree : schema_tree.Tree), certificate_check.text p (toStr "hash") = ok (.Ok g.hash) ∧ strOf g.hash = ok hashS ∧ certificate_check.namespace_of hashS = ok g.nsS ∧ strOf g.nsS = ok g.ns ∧ certificate_check.field p (toStr "tree") = ok (.Ok treeV) ∧ schema_tree.Tree.from_value treeV = ok (.Ok tree) ∧ translation.translate tree profile g.ns = ok (.Ok g.base) ∧ g.φ = g.base ∧ clause_form.clauses g.φ g.ns = ok (.Ok g.cs) /-- `g` is what the kernel computed for the certificate's goal: its tree translates in its hash's namespace, like a premise's, so a goal identical to a premise names the same individuals; its Skolem names are issued in `target`, a namespace no premise has; and its formula is negated when the certificate claims a proof. -/ def GoalOf (cert : Value) (proved : Bool) (profile : working_graph.Profile) (g : Group) : Prop := ∃ (goalV treeV : Value) (tree : schema_tree.Tree) (hashS : Str) (nsS : String) (ns : Str), certificate_check.field cert (toStr "goal") = ok (.Ok goalV) ∧ g.ns = toStr "target" ∧ g.nsS = "target" ∧ certificate_check.text goalV (toStr "hash") = ok (.Ok g.hash) ∧ strOf g.hash = ok hashS ∧ certificate_check.namespace_of hashS = ok nsS ∧ strOf nsS = ok ns ∧ certificate_check.field goalV (toStr "tree") = ok (.Ok treeV) ∧ schema_tree.Tree.from_value treeV = ok (.Ok tree) ∧ translation.translate tree profile ns = ok (.Ok g.base) ∧ g.φ = (if proved then .Not g.base else g.base) ∧ clause_form.clauses g.φ (toStr "target") = ok (.Ok g.cs) /-- The hash discipline, as this theorem needs it: groups in the same namespace translate to the same formula, and groups with the same hash have the same tree, so the translator's output (before any negation) is the same. -/ def Consistent (groups : List Group) : Prop := ∀ g1 ∈ groups, ∀ g2 ∈ groups, (g1.nsS = g2.nsS → g1.φ = g2.φ) ∧ (g1.hash = g2.hash → g1.base = g2.base) theorem Consistent.tail (g : Group) (groups : List Group) (h : Consistent (g :: groups)) : Consistent groups := fun g1 h1 g2 h2 => h g1 (List.mem_cons_of_mem _ h1) g2 (List.mem_cons_of_mem _ h2) /-- The bytes of the empty string. ```lean theorem strOf_empty_val (s : Str) (h : strOf "" = ok s) : s.val = [] ``` #### `group_ns_ok` ```lean theorem group_ns_ok (g : Group) (hns : strOf g.nsS = ok g.ns) (hcl : clause_form.clauses g.φ g.ns = ok (.Ok g.cs)) : g.NsOk ``` #### `group_names_own` ```lean theorem group_names_own (g : Group) (hns : strOf g.nsS = ok g.ns) (hcl : clause_form.clauses g.φ g.ns = ok (.Ok g.cs)) : g.NamesOwn ``` #### `group_holds` ```lean theorem group_holds (g : Group) (hns : strOf g.nsS = ok g.ns) (hcl : clause_form.clauses g.φ g.ns = ok (.Ok g.cs)) (M : Sheaf.Structure Value Value) (hφ : (formulaToSpec g.φ).true M) : g.Holds M ``` #### `check_premise_spec` ```lean theorem check_premise_spec (p : Value) (profile : working_graph.Profile) (clauses clauses1 : KMap) (ph ph1 : sorted_collections.Map String String) (h : certificate_check.check_premise p profile clauses ph = ok (.Ok (), clauses1, ph1)) : ∃ g : Group, PremiseOf p profile g ∧ (∀ c ∈ values clauses1, c ∈ values clauses ∨ c ∈ g.cs.val) ∧ ∀ e ∈ ph1.entries.val, e ∈ ph.entries.val ∨ e.2 = g.hash ``` #### `check_premises_loop_failure` ```lean theorem check_premises_loop_failure (premises : Slice Value) (profile : working_graph.Profile) (clauses : KMap) (ph : sorted_collections.Map String String) (e : certificate_check.Verdict) (index : Usize) (out : KMap × sorted_collections.Map String String × Option certificate_check.Verdict) (h : certificate_check.check_premises_loop premises profile clauses ph (some e) index = ok out) : out.2.2 = some e ``` #### `check_premises_loop_spec` ```lean theorem check_premises_loop_spec (premises : Slice Value) (profile : working_graph.Profile) : ∀ (k : Nat) (clauses clauses1 : KMap) (ph ph1 : sorted_collections.Map String String) (index : Usize), premises.length - index.val = k → certificate_check.check_premises_loop premises profile clauses ph none index = ok (clauses1, ph1, none) → ∃ groups : List Group, (∀ g ∈ groups, ∃ p ∈ premises.val, PremiseOf p profile g) ∧ (∀ c ∈ values clauses1, c ∈ values clauses ∨ ∃ g ∈ groups, c ∈ g.cs.val) ∧ ∀ e ∈ ph1.entries.val, e ∈ ph.entries.val ∨ ∃ g ∈ groups, e.2 = g.hash ``` #### `check_premises_spec` ```lean theorem check_premises_spec (premises : Slice Value) (profile : working_graph.Profile) (clauses clauses1 : KMap) (ph ph1 : sorted_collections.Map String String) (h : certificate_check.check_premises premises profile clauses ph = ok (.Ok (), clauses1, ph1)) : ∃ groups : List Group, (∀ g ∈ groups, ∃ p ∈ premises.val, PremiseOf p profile g) ∧ (∀ c ∈ values clauses1, c ∈ values clauses ∨ ∃ g ∈ groups, c ∈ g.cs.val) ∧ ∀ e ∈ ph1.entries.val, e ∈ ph.entries.val ∨ ∃ g ∈ groups, e.2 = g.hash ``` #### `goal_polarity_spec` ```lean theorem goal_polarity_spec (goal : Value) (proved negated : Bool) (h : certificate_check.goal_polarity goal proved = ok (.Ok negated)) : negated = proved ``` #### `check_goal_spec` ```lean theorem check_goal_spec (cert : Value) (proved : Bool) (profile : working_graph.Profile) (clauses leaves : KMap) (goal_hash : String) (h : certificate_check.check_goal cert proved profile clauses = ok (.Ok goal_hash, leaves)) : ∃ g : Group, GoalOf cert proved profile g ∧ (∀ c ∈ values leaves, c ∈ values clauses ∨ c ∈ g.cs.val) ∧ goal_hash = (if proved then g.hash else "") ``` #### `premise_ns_ne_target` ```lean theorem premise_ns_ne_target (p : Value) (profile : working_graph.Profile) (g : Group) (hg : PremiseOf p profile g) : g.nsS ≠ "target" ``` #### `shared_clauses` Groups that share a namespace share their clauses, given `Consistent`. ```lean theorem shared_clauses (groups : List Group) (hcons : Consistent groups) (hok : ∀ g ∈ groups, strOf g.nsS = ok g.ns ∧ clause_form.clauses g.φ g.ns = ok (.Ok g.cs)) : ∀ g1 ∈ groups, ∀ g2 ∈ groups, g1.nsS = g2.nsS → g1.cs = g2.cs ``` #### `leaves_hold` The leaves hold in some extension of `M` by witness functions when every group's formula is true in `M`. ```lean theorem leaves_hold (M : Sheaf.Structure Value Value) (groups : List Group) (hok : ∀ g ∈ groups, strOf g.nsS = ok g.ns ∧ clause_form.clauses g.φ g.ns = ok (.Ok g.cs)) (hshare : ∀ g1 ∈ groups, ∀ g2 ∈ groups, g1.nsS = g2.nsS → g1.cs = g2.cs) (htrue : ∀ g ∈ groups, (formulaToSpec g.φ).true M) : ∃ fs : String → Option (List M.D → M.D), ∀ g ∈ groups, ∀ c ∈ g.cs.val, (clauseToSpec c).true (M.withSkolems fs) ``` #### `certificate_sound` **What an accepted certificate says.** Its premises are the trees of the `premises` list, each translated in its hash's namespace. Under the hash discipline (`Consistent`): with no goal, the premise formulas have no model; with a goal, no model of the premise formulas satisfies the goal's clause-form formula (the negated goal for a proof, the goal itself for a disproof). ```lean theorem certificate_sound (cert : Value) (v : certificate_check.Verdict) (h : certificate_check.check_inner cert = ok (.Ok v)) : ∃ (profile : working_graph.Profile) (premises : alloc.vec.Vec Value) (groups : List Group) (steps : alloc.vec.Vec Value), certificate_check.read_profile cert = ok (.Ok profile) ∧ certificate_check.list_field cert (toStr "premises") (toStr "premises") = ok (.Ok premises) ∧ (∀ g ∈ groups, ∃ p ∈ premises.val, PremiseOf p profile g) ∧ certificate_check.list_field cert (toStr "steps") (toStr "steps") = ok (.Ok steps) ∧ ((Consistent groups → ∀ M : Sheaf.Structure Value Value, ¬ ∀ g ∈ groups, (formulaToSpec g.φ).true M) ∨ ∃ (proved : Bool) (gg : Group), GoalOf cert proved profile gg ∧ (Consistent (gg :: groups) → ∀ M : Sheaf.Structure Value Value, (∀ g ∈ groups, (formulaToSpec g.φ).true M) → ¬ (formulaToSpec gg.φ).true M)) ``` ### `SheafKernel/Translator.lean` **The translator's operator layer** `certificate_sound` says an accepted certificate's formulas, as the kernel's translator produces them, have no model. This module starts on the remaining link (plan §2.4): what those formulas are. It characterizes the operator layer of `SHEAF/semantics.md` §4.1 and §4.7 directly on the extracted translator: - a binder (`all`, `exists`) translates to `∀x. R → B` / `∃x. R ∧ B`, where `x` is the namespace-qualified variable of the operator's variable occurrence, `R` is the restrictor's atom and `B` the body's formula, both under the environment that binds the variable, its restrictor, its reference and every mention of their referents (`bind_spec`), and nothing else; - `not`, `and`, `or`, `implies` translate to the connective over the operands' formulas in order; - the counting and opaque operators translate to one qualified atom over the restriction and body (or the operands), the bound variable abstracted; - the whole tree is the conjunction of the formulas of its logical roots, each translated under the empty environment (`compile_spec`). The atoms themselves (§4.3–4.5) and the graph the tree is read into are the translator's remaining trusted part; the theorems here take the kernel's own `atom` as the leaf. #### `kind_eq_spec` A kernel string equals a literal exactly when it is that literal. ```lean theorem kind_eq_spec (kind : String) (lit : String) (hlit : lit.toByteArray.size ≤ U32.max) (k : Str) (hk : alloc.string.String.as_str kind = ok k) (b : Bool) (hb : Str.Insts.CoreCmpPartialEqStr.eq k (toStr lit hlit) = ok b) : b = true ↔ kind = lit ``` #### `role_text_spec` ```lean theorem role_text_spec (role : Option String) (r : String) (h : translation.role_text role = ok r) : r = role.getD "" ``` #### `first_or_empty_spec` ```lean theorem first_or_empty_spec (items : Slice String) (r : String) (h : translation.first_or_empty items = ok r) : r = (items.val.head?).getD "" ``` #### `connective_not` ```lean theorem connective_not (p : clause_form.Formula) (parts : alloc.vec.Vec clause_form.Formula) (hparts : parts.val = [p]) (f : clause_form.Formula) (h : translation.connective (toStr "not") parts = ok f) : f = .Not p ``` #### `connective_and` ```lean theorem connective_and (parts : alloc.vec.Vec clause_form.Formula) (f : clause_form.Formula) (h : translation.connective (toStr "and") parts = ok f) : f = .And parts ``` #### `lit_ne` Two different literals compare unequal. ```lean theorem lit_ne (s l : String) (hs : s.toByteArray.size ≤ U32.max) (hl : l.toByteArray.size ≤ U32.max) (hne : s ≠ l) (b : Bool) (hb : Str.Insts.CoreCmpPartialEqStr.eq (toStr s hs) (toStr l hl) = ok b) : b = false ``` #### `connective_or` ```lean theorem connective_or (parts : alloc.vec.Vec clause_form.Formula) (f : clause_form.Formula) (h : translation.connective (toStr "or") parts = ok f) : f = .Or parts ``` #### `connective_implies` ```lean theorem connective_implies (a c : clause_form.Formula) (parts : alloc.vec.Vec clause_form.Formula) (hparts : parts.val = [a, c]) (f : clause_form.Formula) (h : translation.connective (toStr "implies") parts = ok f) : f = .Implies a c ``` #### `variable_spec` A binder's variable is the namespace-qualified name of its variable occurrence. ```lean theorem variable_spec (self : translation.Translator) («name» : Str) (t : first_order.Term) (h : translation.Translator.variable self «name» = ok t) : ∃ nameS : String, decodeUtf8 «name».val = some nameS ∧ t = .Var (self.namespace ++ ":" ++ nameS) ``` #### `restricted_spec` `restricted`: the restrictor occurrence's atom and the first operand's formula, both under the bound environment, in that order. ```lean theorem restricted_spec (self : translation.Translator) (op : working_graph.Operator) (inner : TEnv) (fuel : U32) (R B : clause_form.Formula) (self2 : translation.Translator) (h : translation.Translator.restricted self op inner fuel = ok (.Ok (R, B), self2)) : ∃ (rs bs : Str) (self1 : translation.Translator), strOf (op.restrictor.getD "") = ok rs ∧ strOf (((alloc.vec.Vec.deref op.operands).val.head?).getD "") = ok bs ∧ translation.Translator.atom self rs inner (toStr "") (toStr "") (toStr "") fuel = ok (.Ok R, self1) ∧ translation.Translator.formula self1 bs inner fuel = ok (.Ok B, self2) ``` #### `formula_all` The kernel's lookup of an operator by its key. -/ abbrev opOf (self : translation.Translator) (key : Str) := sorted_collections.Map.cloned alloc.string.String.Insts.CoreCmpOrd Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr working_graph.Operator.Insts.CoreCloneClone self.ops key /-- **`all`**: `∀x. R → B`, with `x` the binder's variable, `R` the restrictor's atom and `B` the body's formula, both under the environment `bind` extends. ```lean theorem formula_all (self self' : translation.Translator) (key : Str) (env : TEnv) (fuel : U32) (φ : clause_form.Formula) (op : working_graph.Operator) (h : translation.Translator.formula self key env fuel = ok (.Ok φ, self')) (hop : opOf self key = ok (some op)) (hall : op.operation = "all") : ∃ (f : U32) («name» : String) (inner : TEnv) (R B : clause_form.Formula), U32.checked_sub fuel 1#u32 = some f ∧ translation.Translator.bind self op env = ok (.Var «name», inner) ∧ translation.Translator.restricted self op inner f = ok (.Ok (R, B), self') ∧ φ = .All «name» (.Implies R B) ``` #### `formula_exists` **`exists`**: `∃x. R ∧ B`, the conjunction's two parts in that order. ```lean theorem formula_exists (self self' : translation.Translator) (key : Str) (env : TEnv) (fuel : U32) (φ : clause_form.Formula) (op : working_graph.Operator) (h : translation.Translator.formula self key env fuel = ok (.Ok φ, self')) (hop : opOf self key = ok (some op)) (hk : op.operation = "exists") : ∃ (f : U32) («name» : String) (inner : TEnv) (R B : clause_form.Formula) (parts : alloc.vec.Vec clause_form.Formula), U32.checked_sub fuel 1#u32 = some f ∧ translation.Translator.bind self op env = ok (.Var «name», inner) ∧ translation.Translator.restricted self op inner f = ok (.Ok (R, B), self') ∧ parts.val = [R, B] ∧ φ = .Exists «name» (.And parts) ``` #### `formula_connective` A connective operator's formula is the connective over its operands' formulas, in order. ```lean theorem formula_connective (self self' : translation.Translator) (key : Str) (env : TEnv) (fuel : U32) (φ : clause_form.Formula) (op : working_graph.Operator) (h : translation.Translator.formula self key env fuel = ok (.Ok φ, self')) (hop : opOf self key = ok (some op)) (hk : op.operation = "not" ∨ op.operation = "and" ∨ op.operation = "or" ∨ op.operation = "implies") : ∃ (f : U32) (kind : Str) (parts : alloc.vec.Vec clause_form.Formula), U32.checked_sub fuel 1#u32 = some f ∧ alloc.string.String.as_str op.operation = ok kind ∧ translation.Translator.operand_formulas self (alloc.vec.Vec.deref op.operands) env f = ok (.Ok parts, self') ∧ translation.connective kind parts = ok φ ``` #### `formula_counting` A counting operator is one qualified atom over its restriction and body, the bound variable abstracted; the restriction and body are the binder's, under the bound environment, exactly as for `all` and `exists`. ```lean theorem formula_counting (self self' : translation.Translator) (key : Str) (env : TEnv) (fuel : U32) (φ : clause_form.Formula) (op : working_graph.Operator) (h : translation.Translator.formula self key env fuel = ok (.Ok φ, self')) (hop : opOf self key = ok (some op)) (hk : op.operation = "most" ∨ op.operation = "few" ∨ op.operation = "many" ∨ op.operation = "several" ∨ op.operation = "exactly" ∨ op.operation = "at_least" ∨ op.operation = "at_most") : ∃ (f : U32) (kind : Str) («variable» : first_order.Term) (inner : TEnv) (R B : clause_form.Formula) (formulas : alloc.vec.Vec clause_form.Formula) (bound : alloc.vec.Vec first_order.Term), U32.checked_sub fuel 1#u32 = some f ∧ alloc.string.String.as_str op.operation = ok kind ∧ translation.Translator.bind self op env = ok («variable», inner) ∧ translation.Translator.restricted self op inner f = ok (.Ok (R, B), self') ∧ formulas.val = [R, B] ∧ bound.val = [«variable»] ∧ translation.qualify (alloc.vec.Vec.deref formulas) kind op.cardinality (alloc.vec.Vec.deref bound) = ok φ ``` #### `map_insert_binds` `k` is bound to `v` in the environment. -/ def Binds (m : TEnv) (k : String) (v : first_order.Term) : Prop := ∃ e ∈ m.entries.val, e.1 = k ∧ e.2 = v /-- After `insert k v`, `k` is bound to `v`. ```lean theorem map_insert_binds (m : TEnv) (k : String) (v : first_order.Term) (p : Option first_order.Term × TEnv) (h : sorted_collections.Map.insert alloc.string.String.Insts.CoreCmpOrd m k v = ok p) : Binds p.2 k v ``` #### `map_insert_keeps_binding` `insert k' v` keeps every binding to the same `v`. ```lean theorem map_insert_keeps_binding (m : TEnv) (k' : String) (v : first_order.Term) (p : Option first_order.Term × TEnv) (h : sorted_collections.Map.insert alloc.string.String.Insts.CoreCmpOrd m k' v = ok p) (k : String) (hb : Binds m k v) : Binds p.2 k v ``` #### `bind_key_loop_spec` `bind_key_loop` binds every mention from `k` on to the variable, keeps every binding to it, and introduces nothing else. ```lean theorem bind_key_loop_spec («variable» : first_order.Term) (mentions : alloc.vec.Vec String) : ∀ (n : Nat) (inner inner' : TEnv) (k : Usize), mentions.val.length - k.val = n → translation.Translator.bind_key_loop «variable» inner mentions k = ok inner' → (∀ i, k.val ≤ i → ∀ m, mentions.val[i]? = some m → Binds inner' m «variable») ∧ (∀ key, Binds inner key «variable» → Binds inner' key «variable») ∧ (∀ e ∈ inner'.entries.val, e ∈ inner.entries.val ∨ e.2 = «variable») ``` #### `bind_key_spec` The kernel's lookup of a key's referent, and of a referent's mentions. -/ abbrev referentOf (self : translation.Translator) (key : Str) := sorted_collections.Map.get alloc.string.String.Insts.CoreCmpOrd Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr self.refs key abbrev mentionsOf (self : translation.Translator) (referent : String) := sorted_collections.Map.cloned_or_default alloc.string.String.Insts.CoreCmpOrd alloc.string.String.Insts.CoreCmpOrd (core.borrow.Borrow.Blanket String) (core.clone.CloneallocvecVec alloc.string.String.Insts.CoreCloneClone) (alloc.vec.Vec.Insts.CoreDefaultDefault String) self.mentions referent /-- **`bind_key`**: the key and every mention of its referent are bound to the variable; existing bindings to the variable stay; nothing else is introduced. ```lean theorem bind_key_spec (self : translation.Translator) (key : Str) («variable» : first_order.Term) (inner inner' : TEnv) (h : translation.Translator.bind_key self key «variable» inner = ok inner') : ∃ keyS : String, decodeUtf8 key.val = some keyS ∧ Binds inner' keyS «variable» ∧ (∀ k, Binds inner k «variable» → Binds inner' k «variable») ∧ (∀ e ∈ inner'.entries.val, e ∈ inner.entries.val ∨ e.2 = «variable») ∧ (∀ referent, referentOf self key = ok (some referent) → ∀ mentions, mentionsOf self referent = ok mentions → ∀ m ∈ mentions.val, Binds inner' m «variable») ``` #### `bind_loop_spec` `bind_loop` binds every key from `index` on (with its referent's mentions), keeps bindings to the variable and introduces nothing else. ```lean theorem bind_loop_spec (self : translation.Translator) («variable» : first_order.Term) (keys : alloc.vec.Vec String) : ∀ (n : Nat) (inner inner' : TEnv) (index : Usize), keys.val.length - index.val = n → translation.Translator.bind_loop self «variable» inner keys index = ok inner' → (∀ i, index.val ≤ i → ∀ k, keys.val[i]? = some k → Binds inner' k «variable» ∧ ∀ ks, strOf k = ok ks → ∀ referent, referentOf self ks = ok (some referent) → ∀ mentions, mentionsOf self referent = ok mentions → ∀ m ∈ mentions.val, Binds inner' m «variable») ∧ (∀ k, Binds inner k «variable» → Binds inner' k «variable») ∧ (∀ e ∈ inner'.entries.val, e ∈ inner.entries.val ∨ e.2 = «variable») ``` #### `bind_spec` The occurrences a binder binds: its variable, its restrictor and its reference. -/ def bindKeys (op : working_graph.Operator) : List String := [op.variable.getD ""] ++ op.restrictor.toList ++ op.reference.toList /-- **`bind`** (§4.1): the variable is the namespace-qualified name of the operator's variable occurrence; the variable, restrictor and reference occurrences and every mention of their referents are bound to it; every other binding is the enclosing environment's. Binding follows references, never tree edges. ```lean theorem bind_spec (self : translation.Translator) (op : working_graph.Operator) (env : TEnv) («variable» : first_order.Term) (inner : TEnv) (h : translation.Translator.bind self op env = ok («variable», inner)) : «variable» = .Var (self.namespace ++ ":" ++ op.variable.getD "") ∧ (∀ k ∈ bindKeys op, Binds inner k «variable» ∧ ∀ ks, strOf k = ok ks → ∀ referent, referentOf self ks = ok (some referent) → ∀ mentions, mentionsOf self referent = ok mentions → ∀ m ∈ mentions.val, Binds inner m «variable») ∧ (∀ e ∈ inner.entries.val, e ∈ env.entries.val ∨ e.2 = «variable») ``` #### `operand_formulas_spec` The formulas of a list of occurrence keys, translated one after another: each from the translator state the previous one left (only `reached` and `reifying` ever change). -/ inductive FormulaChain (env : TEnv) (fuel : U32) : translation.Translator → List String → List clause_form.Formula → translation.Translator → Prop | nil (t : translation.Translator) : FormulaChain env fuel t [] [] t | cons (t t1 t2 : translation.Translator) (k : String) (ks : Str) (φ : clause_form.Formula) (rest : List String) (φs : List clause_form.Formula) : strOf k = ok ks → translation.Translator.formula t ks env fuel = ok (.Ok φ, t1) → FormulaChain env fuel t1 rest φs t2 → FormulaChain env fuel t (k :: rest) (φ :: φs) t2 theorem operand_formulas_loop_failure (self : translation.Translator) (operands : Slice String) (env : TEnv) (fuel : U32) (parts : alloc.vec.Vec clause_form.Formula) (e : schema_tree.TreeError) (index : Usize) (out : translation.Translator × alloc.vec.Vec clause_form.Formula × Option schema_tree.TreeError) (h : translation.Translator.operand_formulas_loop self operands env fuel parts (some e) index = ok out) : out.2.2 = some e := by unfold translation.Translator.operand_formulas_loop at h dsimp only at h split at h · simp only [core.option.Option.is_none] at h split at h · rename_i hb exact absurd hb (by simp) · rw [ok_eq_ok_iff] at h rw [← h] · rw [ok_eq_ok_iff] at h rw [← h] theorem operand_formulas_loop_spec (operands : Slice String) (env : TEnv) (fuel : U32) : ∀ (n : Nat) (self self' : translation.Translator) (parts parts' : alloc.vec.Vec clause_form.Formula) (index : Usize), operands.val.length - index.val = n → translation.Translator.operand_formulas_loop self operands env fuel parts none index = ok (self', parts', none) → ∃ φs, parts'.val = parts.val ++ φs ∧ FormulaChain env fuel self (operands.val.drop index.val) φs self' := by intro n induction n with | zero => intro self self' parts parts' index hk h unfold translation.Translator.operand_formulas_loop at h dsimp only at h have hlen : operands.length = operands.val.length := rfl have hlen' := Slice.len_val operands split at h · exfalso rename_i hlt scalar_tac · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h obtain ⟨hs, hp, _⟩ := h subst hs hp refine ⟨[], by simp, ?_⟩ rw [List.drop_of_length_le (by omega)] exact FormulaChain.nil _ | succ n ih => intro self self' parts parts' index hk h unfold translation.Translator.operand_formulas_loop at h dsimp only at h have hlen : operands.length = operands.val.length := rfl have hlen' := Slice.len_val operands split at h · rename_i hlt rw [if_pos (show core.option.Option.is_none (none : Option schema_tree.TreeError) = true from rfl)] at h read_ok at h obtain ⟨s, hs, s1, hs1, q, hq, pf, hpf, h⟩ := h obtain ⟨r, self1⟩ := q obtain ⟨parts1, failure1⟩ := pf dsimp only at hq hpf h have hs' := slice_index_usize_eq_ok _ _ _ hs unfold alloc.string.String.Insts.CoreOpsDerefDerefStr.deref at hs1 have hlt' : index.val < operands.val.length := by scalar_tac have hidx : (core.num.Usize.wrapping_add index 1#usize).val = index.val + 1 := usize_succ_val index operands.val.length hlt' operands.property cases r with | Err e => dsimp only at hpf try rw [ok_eq_ok_iff] at hpf simp only [Prod.mk.injEq] at hpf obtain ⟨_, hf⟩ := hpf subst hf exfalso have := operand_formulas_loop_failure _ _ _ _ _ _ _ _ h simp at this | Ok part => dsimp only at hpf read_ok at hpf obtain ⟨parts2, hparts2, hpf⟩ := hpf try rw [ok_eq_ok_iff] at hpf simp only [Prod.mk.injEq] at hpf obtain ⟨hp2, hf⟩ := hpf subst hp2 hf obtain ⟨φs, hparts', hchain⟩ := ih self1 self' parts2 parts' _ (by omega) h refine ⟨part :: φs, ?_, ?_⟩ · rw [hparts', vec_push_eq_ok _ _ _ hparts2] simp · have hdrop : operands.val.drop index.val = s :: operands.val.drop (index.val + 1) := by rw [List.drop_eq_getElem_cons hlt'] rw [(List.getElem?_eq_some_iff.mp hs').2] rw [hdrop] rw [hidx] at hchain exact FormulaChain.cons self self1 self' s s1 part _ φs hs1 hq hchain · exfalso rename_i hge scalar_tac /-- **`operand_formulas`**: one formula per operand, in order. ```lean theorem operand_formulas_spec (self self' : translation.Translator) (operands : Slice String) (env : TEnv) (fuel : U32) (parts : alloc.vec.Vec clause_form.Formula) (h : translation.Translator.operand_formulas self operands env fuel = ok (.Ok parts, self')) : FormulaChain env fuel self operands.val parts.val self' ``` #### `map_remove_mem` What `remove` returns was an entry's value. ```lean theorem map_remove_mem {V Q : Type} (inst1 : core.cmp.Ord Q) (binst : core.borrow.Borrow String Q) (m : sorted_collections.Map String V) (key : Q) (v : V) (m' : sorted_collections.Map String V) (h : sorted_collections.Map.remove alloc.string.String.Insts.CoreCmpOrd inst1 binst m key = ok (some v, m')) : (∃ k, (k, v) ∈ m.entries.val) ∧ ∀ e ∈ m'.entries.val, e ∈ m.entries.val ``` #### `compile_spec` A part of the conjunction: the formula of one logical root under the empty environment, from some translator state of the walk. -/ def RootFormula (self : translation.Translator) (env : TEnv) (p : clause_form.Formula) : Prop := ∃ root ∈ self.logic_roots.val, ∃ (rs : Str) (t t' : translation.Translator), strOf root = ok rs ∧ translation.Translator.formula t rs env translation.TRANSLATE_FUEL = ok (.Ok p, t') theorem compile_loop1_failure (self : translation.Translator) (roots : alloc.vec.Vec String) (er : sorted_collections.Set String) (env : TEnv) (formulas : sorted_collections.Map String clause_form.Formula) (e : schema_tree.TreeError) (index : Usize) (out : translation.Translator × sorted_collections.Map String clause_form.Formula × Option schema_tree.TreeError) (h : translation.Translator.compile_loop1 self roots er env formulas (some e) index = ok out) : out.2.2 = some e := by unfold translation.Translator.compile_loop1 at h dsimp only at h split at h · simp only [core.option.Option.is_none] at h split at h · rename_i hb exact absurd hb (by simp) · rw [ok_eq_ok_iff] at h rw [← h] · rw [ok_eq_ok_iff] at h rw [← h] theorem compile_loop2_failure (self : translation.Translator) (roots : alloc.vec.Vec String) (env : TEnv) (formulas : sorted_collections.Map String clause_form.Formula) (parts : alloc.vec.Vec clause_form.Formula) (e : schema_tree.TreeError) (index : Usize) (out : translation.Translator × alloc.vec.Vec clause_form.Formula × Option schema_tree.TreeError) (h : translation.Translator.compile_loop2 self roots env formulas parts (some e) index = ok out) : out.2.2 = some e := by unfold translation.Translator.compile_loop2 at h dsimp only at h split at h · simp only [core.option.Option.is_none] at h split at h · rename_i hb exact absurd hb (by simp) · rw [ok_eq_ok_iff] at h rw [← h] · rw [ok_eq_ok_iff] at h rw [← h] /-- Every formula the first pass stores is a root's formula. -/ def StoredRoots (self0 : translation.Translator) (env : TEnv) (formulas : sorted_collections.Map String clause_form.Formula) : Prop := ∀ e ∈ formulas.entries.val, RootFormula self0 env e.2 theorem compile_loop1_spec (self0 : translation.Translator) (er : sorted_collections.Set String) (env : TEnv) : ∀ (n : Nat) (self self' : translation.Translator) (roots : alloc.vec.Vec String) (formulas formulas' : sorted_collections.Map String clause_form.Formula) (index : Usize), roots.val = self0.logic_roots.val → roots.val.length - index.val = n → StoredRoots self0 env formulas → translation.Translator.compile_loop1 self roots er env formulas none index = ok (self', formulas', none) → StoredRoots self0 env formulas' := by intro n induction n with | zero => intro self self' roots formulas formulas' index hr hk hinv h unfold translation.Translator.compile_loop1 at h dsimp only at h have hlen : roots.length = roots.val.length := rfl have hlen' := alloc.vec.Vec.len_val roots split at h · exfalso rename_i hlt scalar_tac · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h obtain ⟨_, hf, _⟩ := h subst hf exact hinv | succ n ih => intro self self' roots formulas formulas' index hr hk hinv h unfold translation.Translator.compile_loop1 at h dsimp only at h have hlen : roots.length = roots.val.length := rfl have hlen' := alloc.vec.Vec.len_val roots split at h · rename_i hlt rw [if_pos (show core.option.Option.is_none (none : Option schema_tree.TreeError) = true from rfl)] at h read_ok at h obtain ⟨s, hs, b1, hb1, q, hq, h⟩ := h obtain ⟨self1, formulas1, failure1⟩ := q dsimp only at hq h rw [alloc.vec.Vec.index_slice_index] at hs have hs' := vec_index_usize_eq_ok _ _ _ hs have hlt' : index.val < roots.val.length := by scalar_tac have hidx : (core.num.Usize.wrapping_add index 1#usize).val = index.val + 1 := usize_succ_val index roots.val.length hlt' roots.property have hmem : s ∈ self0.logic_roots.val := by rw [← hr] exact List.mem_of_getElem? hs' -- the stored map after this root have hinv1 : failure1 = none → StoredRoots self0 env formulas1 := by intro hnone subst hnone cases b1 with | true => simp only [↓reduceIte, ok_eq_ok_iff, Prod.mk.injEq] at hq obtain ⟨_, hf, _⟩ := hq subst hf exact hinv | false => simp only [Bool.false_eq_true, ↓reduceIte] at hq read_ok at hq obtain ⟨s1, hs1, q2, hq2, mo, hmo, hq⟩ := hq obtain ⟨r, self2⟩ := q2 obtain ⟨m, o⟩ := mo dsimp only at hq2 hmo hq unfold alloc.string.String.Insts.CoreOpsDerefDerefStr.deref at hs1 try rw [ok_eq_ok_iff] at hq simp only [Prod.mk.injEq] at hq obtain ⟨_, hm, ho⟩ := hq subst hm ho cases r with | Ok φ => dsimp only at hmo read_ok at hmo obtain ⟨s2, hs2, p, hp, hmo⟩ := hmo rw [string_clone_eq _ _ hs2] at hp simp only [ok_eq_ok_iff, Prod.mk.injEq] at hmo obtain ⟨hm, _⟩ := hmo subst hm intro e he rcases map_insert_entries formulas s φ p hp e he with hv | hin · rw [hv] exact ⟨s, hmem, s1, self, self2, hs1, hq2⟩ · exact hinv e hin | Err e => dsimp only at hmo simp at hmo -- the loop could only have continued without a failure cases hf1 : failure1 with | some e => exfalso rw [hf1] at h have := compile_loop1_failure _ _ _ _ _ _ _ _ h simp at this | none => rw [hf1] at h exact ih self1 self' roots formulas1 formulas' _ hr (by omega) (hinv1 hf1) h · exfalso rename_i hge scalar_tac theorem root_formula_spec (self0 self self1 : translation.Translator) (root : Str) (env : TEnv) (formulas formulas1 : sorted_collections.Map String clause_form.Formula) (φ : clause_form.Formula) (hinv : StoredRoots self0 env formulas) (rootS : String) (hroot : strOf rootS = ok root) (hmem : rootS ∈ self0.logic_roots.val) (h : translation.Translator.root_formula self root formulas env = ok (.Ok φ, self1, formulas1)) : RootFormula self0 env φ ∧ StoredRoots self0 env formulas1 := by unfold translation.Translator.root_formula at h read_ok at h obtain ⟨p, hp, h⟩ := h obtain ⟨o, formulas1'⟩ := p dsimp only at hp h cases o with | none => read_ok at h obtain ⟨q, hq, h⟩ := h obtain ⟨r, self1'⟩ := q dsimp only at hq h try rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h obtain ⟨hr, _, hf⟩ := h subst hr hf refine ⟨⟨rootS, hmem, root, self, self1', hroot, hq⟩, ?_⟩ -- removing nothing keeps the map's entries unfold sorted_collections.Map.remove at hp read_ok at hp obtain ⟨q, hq', hp⟩ := hp split at hp · unfold alloc.vec.Vec.remove at hp split at hp · simp at hp · simp at hp · rw [ok_eq_ok_iff] at hp simp only [Prod.mk.injEq] at hp obtain ⟨_, hm⟩ := hp subst hm exact hinv | some f => dsimp only at h rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq, core.result.Result.Ok.injEq] at h obtain ⟨hf, _, hm⟩ := h subst hf hm obtain ⟨⟨k, hk⟩, hsub⟩ := map_remove_mem _ _ formulas root f formulas1' hp exact ⟨hinv (k, f) hk, fun e he => hinv e (hsub e he)⟩ theorem compile_loop2_spec (self0 : translation.Translator) (env : TEnv) : ∀ (n : Nat) (self self' : translation.Translator) (roots : alloc.vec.Vec String) (formulas : sorted_collections.Map String clause_form.Formula) (parts parts' : alloc.vec.Vec clause_form.Formula) (index : Usize), roots.val = self0.logic_roots.val → roots.val.length - index.val = n → StoredRoots self0 env formulas → (∀ p ∈ parts.val, RootFormula self0 env p) → translation.Translator.compile_loop2 self roots env formulas parts none index = ok (self', parts', none) → ∀ p ∈ parts'.val, RootFormula self0 env p := by intro n induction n with | zero => intro self self' roots formulas parts parts' index hr hk hinv hparts h unfold translation.Translator.compile_loop2 at h dsimp only at h have hlen : roots.length = roots.val.length := rfl have hlen' := alloc.vec.Vec.len_val roots split at h · exfalso rename_i hlt scalar_tac · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h obtain ⟨_, hp, _⟩ := h subst hp exact hparts | succ n ih => intro self self' roots formulas parts parts' index hr hk hinv hparts h unfold translation.Translator.compile_loop2 at h dsimp only at h have hlen : roots.length = roots.val.length := rfl have hlen' := alloc.vec.Vec.len_val roots split at h · rename_i hlt rw [if_pos (show core.option.Option.is_none (none : Option schema_tree.TreeError) = true from rfl)] at h read_ok at h obtain ⟨s, hs, b1, hb1, q, hq, h⟩ := h obtain ⟨self1, formulas1, parts1, failure1⟩ := q dsimp only at hq h rw [alloc.vec.Vec.index_slice_index] at hs have hs' := vec_index_usize_eq_ok _ _ _ hs have hlt' : index.val < roots.val.length := by scalar_tac have hidx : (core.num.Usize.wrapping_add index 1#usize).val = index.val + 1 := usize_succ_val index roots.val.length hlt' roots.property have hmem : s ∈ self0.logic_roots.val := by rw [← hr] exact List.mem_of_getElem? hs' have hstep : failure1 = none → StoredRoots self0 env formulas1 ∧ ∀ p ∈ parts1.val, RootFormula self0 env p := by intro hnone subst hnone cases b1 with | true => simp only [↓reduceIte, ok_eq_ok_iff, Prod.mk.injEq] at hq obtain ⟨_, hf, hp, _⟩ := hq subst hf hp exact ⟨hinv, hparts⟩ | false => simp only [Bool.false_eq_true, ↓reduceIte] at hq read_ok at hq obtain ⟨s1, hs1, q2, hq2, vo, hvo, hq⟩ := hq obtain ⟨r, self2, formulas2⟩ := q2 obtain ⟨v, o⟩ := vo dsimp only at hq2 hvo hq unfold alloc.string.String.Insts.CoreOpsDerefDerefStr.deref at hs1 try rw [ok_eq_ok_iff] at hq simp only [Prod.mk.injEq] at hq obtain ⟨_, hf, hv, ho⟩ := hq subst hf hv ho cases r with | Ok φ => dsimp only at hvo read_ok at hvo obtain ⟨parts2, hparts2, hvo⟩ := hvo simp only [ok_eq_ok_iff, Prod.mk.injEq] at hvo obtain ⟨hv, _⟩ := hvo subst hv obtain ⟨hφ, hinv2⟩ := root_formula_spec self0 self self2 s1 env formulas formulas2 φ hinv s hs1 hmem hq2 refine ⟨hinv2, ?_⟩ intro p hp rw [vec_push_eq_ok _ _ _ hparts2] at hp rcases List.mem_append.mp hp with hp | hp · exact hparts p hp · rw [List.mem_singleton] at hp subst hp exact hφ | Err e => dsimp only at hvo simp at hvo cases hf1 : failure1 with | some e => exfalso rw [hf1] at h have := compile_loop2_failure _ _ _ _ _ _ _ _ h simp at this | none => rw [hf1] at h obtain ⟨hinv1, hparts1⟩ := hstep hf1 exact ih self1 self' roots formulas1 parts1 parts' _ hr (by omega) hinv1 hparts1 h · exfalso rename_i hge scalar_tac /-- **`compile`** (§4, §4.7): a tree's formula is the conjunction of formulas of its logical roots, each translated under the empty environment; a non-assertion speech act is not translated. ```lean theorem compile_spec (self self' : translation.Translator) (φ : clause_form.Formula) (h : translation.Translator.compile self = ok (.Ok φ, self')) : self.non_assertion = false ∧ ∃ parts : alloc.vec.Vec clause_form.Formula, φ = .And parts ∧ ∀ p ∈ parts.val, RootFormula self { entries ``` #### `translate_spec` **`translate`**: a tree's formula is its working graph's, compiled by a translator built for that graph, the profile and the namespace. ```lean theorem translate_spec (tree : schema_tree.Tree) (profile : working_graph.Profile) (ns : Str) (φ : clause_form.Formula) (h : translation.translate tree profile ns = ok (.Ok φ)) : ∃ (graph : working_graph.Graph) (t t' : translation.Translator), working_graph.graph_from_tree tree profile = ok (.Ok graph) ∧ translation.Translator.new graph profile ns = ok (.Ok t) ∧ translation.Translator.compile t = ok (.Ok φ, t') ``` ### `SheafKernel/Terms.lean` **Terms of occurrences (§4.5)** What an occurrence denotes in the translator's formulas: a bound occurrence is its variable; a verified or unverified name is its name constant; a lexical occurrence with no referent is its occurrence constant in the tree's namespace. The remaining case, an occurrence with a referent (`reference_term`), is read through the bound mentions, the shared verified name, the antecedent clause's proposition or the referent's constant, and is not characterized here yet. #### `map_locate_str_loop_found` The kernel's binary search over a string-keyed map with a `str` key: when it reports `found`, the entry at `at` has the key's decoding as its key. ```lean theorem map_locate_str_loop_found {V : Type} (v : alloc.vec.Vec (String × V)) (key : Str) : ∀ (k : Nat) (low high : Usize) (found : Bool) («at» : Usize), high.val - low.val = k → high.val ≤ v.length → (found = true → ∃ e, v.val[low.val]? = some e ∧ decodeUtf8 key.val = some e.1) → sorted_collections.Map.locate_loop Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr v key low high found = ok (true, «at») → ∃ e, v.val[«at».val]? = some e ∧ decodeUtf8 key.val = some e.1 ``` #### `map_locate_str_found` ```lean theorem map_locate_str_found {V : Type} (m : sorted_collections.Map String V) (key : Str) («at» : Usize) (h : sorted_collections.Map.locate alloc.string.String.Insts.CoreCmpOrd Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr m key = ok (true, «at»)) : ∃ e, m.entries.val[«at».val]? = some e ∧ decodeUtf8 key.val = some e.1 ``` #### `map_cloned_str_spec` What `cloned` finds under a `str` key is the entry of the key's decoding. ```lean theorem map_cloned_str_spec {V : Type} (inst : core.clone.Clone V) (hclone : ∀ x x' : V, inst.clone x = ok x' → x' = x) (m : sorted_collections.Map String V) (key : Str) (v : V) (h : sorted_collections.Map.cloned alloc.string.String.Insts.CoreCmpOrd Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr inst m key = ok (some v)) : ∃ k : String, decodeUtf8 key.val = some k ∧ (k, v) ∈ m.entries.val ``` #### `s_spec` ```lean theorem s_spec (text : Str) (v : Value) (h : translation.s text = ok v) : ∃ t : String, decodeUtf8 text.val = some t ∧ v = .Text t ``` #### `constant_spec` **An occurrence constant** (§2): `["const", [namespace, occurrence]]`. ```lean theorem constant_spec (self : translation.Translator) (key : Str) (t : first_order.Term) (h : translation.Translator.constant self key = ok t) : ∃ (keyS : String) (outer inner : alloc.vec.Vec first_order.Term), decodeUtf8 key.val = some keyS ∧ t = .Node outer ∧ outer.val = [.Atom (.Text "const"), .Node inner] ∧ inner.val = [.Atom (.Text self.namespace), .Atom (.Text keyS)] ``` #### `term_bound` The kernel's lookup of a key in the bound environment. -/ abbrev boundOf (env : TEnv) (key : Str) := sorted_collections.Map.cloned alloc.string.String.Insts.CoreCmpOrd Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr first_order.Term.Insts.CoreCloneClone env key /-- The kernel's lookup of a key's referent, by `str` key. -/ abbrev refOf (self : translation.Translator) (key : Str) := sorted_collections.Map.cloned alloc.string.String.Insts.CoreCmpOrd Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr alloc.string.String.Insts.CoreCloneClone self.refs key /-- **A bound occurrence is its variable**: when the environment binds the key, `term` returns that binding and changes nothing. ```lean theorem term_bound (self self' : translation.Translator) (key : Str) (env : TEnv) (fuel : U32) (t t0 : first_order.Term) (h : translation.Translator.term self key env fuel = ok (.Ok t, self')) (hbound : boundOf env key = ok (some t0)) : t = t0 ∧ self' = self ∧ ∃ keyS, decodeUtf8 key.val = some keyS ∧ Binds env keyS t ``` #### `term_constant` **An unbound lexical occurrence with no referent is its occurrence constant.** ```lean theorem term_constant (self self' : translation.Translator) (key : Str) (env : TEnv) (fuel : U32) (t : first_order.Term) (n : working_graph.GNode) (h : translation.Translator.term self key env fuel = ok (.Ok t, self')) (hfree : boundOf env key = ok none) (hnode : translation.Translator.node self key = ok (.Ok n)) (hkind : n.kind = .Lexical) (hnoref : refOf self key = ok none) : self' = self ∧ translation.Translator.constant self key = ok t ``` #### `term_name` **A name is its name constant**: `["const", identity]`, with the identity `["name", url]` or the document-scoped unverified name (`identity`, §2). ```lean theorem term_name (self self' : translation.Translator) (key : Str) (env : TEnv) (fuel : U32) (t : first_order.Term) (n : working_graph.GNode) (h : translation.Translator.term self key env fuel = ok (.Ok t, self')) (hfree : boundOf env key = ok none) (hnode : translation.Translator.node self key = ok (.Ok n)) (hkind : n.kind = .Name) : self' = self ∧ ∃ (idv : Value) (idt : first_order.Term) (outer : alloc.vec.Vec first_order.Term), translation.identity n = ok (.Ok idv) ∧ translation.value_term idv = ok idt ∧ t = .Node outer ∧ outer.val = [.Atom (.Text "const"), idt] ``` #### `atom_combinator` **A combinator occurrence is its operation over its children's formulas**, in edge order. ```lean theorem atom_combinator (self self' : translation.Translator) (key : Str) (env : TEnv) (claim_of host of : Str) (fuel : U32) (φ : clause_form.Formula) (n : working_graph.GNode) (h : translation.Translator.atom self key env claim_of host of fuel = ok (.Ok φ, self')) (hnode : translation.Translator.node self key = ok (.Ok n)) (hkind : n.kind = .Combinator) : ∃ (f : U32) (children : alloc.vec.Vec String) (parts : alloc.vec.Vec clause_form.Formula) (opS : String) (ops : Str), U32.checked_sub fuel 1#u32 = some f ∧ translation.Translator.children_of self key = ok children ∧ translation.Translator.operand_formulas self (alloc.vec.Vec.deref children) env f = ok (.Ok parts, self') ∧ translation.Translator.operation_of n = ok opS ∧ strOf opS = ok ops ∧ translation.connective ops parts = ok φ ``` #### `reference_term_bound` **A referent some mention of which is bound takes that binding.** ```lean theorem reference_term_bound (self self' : translation.Translator) (referent : Str) (env : TEnv) (fuel : U32) (t t0 : first_order.Term) (h : translation.Translator.reference_term self referent env fuel = ok (.Ok t, self')) (hbound : translation.Translator.bound_mention self referent env = ok (some t0)) : t = t0 ∧ self' = self ``` #### `new_namespace` **`Translator.new` names its constants and variables in the namespace it was given**: the hash's namespace for a premise or a goal (`certificate_check`). ```lean theorem new_namespace (graph : working_graph.Graph) (profile : working_graph.Profile) (ns : Str) (t : translation.Translator) (h : translation.Translator.new graph profile ns = ok (.Ok t)) : decodeUtf8 ns.val = some t.namespace ``` ### `SheafKernel/Atoms.lean` **Atoms (§4.3–4.4)** The leaves of a formula: what the translator asserts of one occurrence. This module characterizes, on the extracted translator, the pieces `SHEAF/semantics.md` §4.3 names: - a predicate symbol is the occurrence's predicate tuple with the ordered roles of its arguments appended (`with_roles_spec`), and a one-place predication adds the single role `theme` (`theme_atom_spec`); - a verb is that predicate over its arguments' terms, in the order of its argument pairs (`verb_atom_spec`); - a noun or adjective is predicated of its subject (itself when unpredicated): the full predicate, the description, or both (`nonverbal_atom_spec`); - the main atom is conjoined with its constraints when there are any (`conjoin_spec`), and a non-declarative clause is wrapped as one qualified proposition (`qualified_by_clause_type_spec`); - a lexical occurrence's atom has exactly that shape: the verb or nonverbal main atom, the edge and possession constraints, the clause-type wrapper (`atom_lexical`). The predicate tuples themselves (`predicates_for`), the edges an atom reads, the constraints' contents and the copula reading (§4.4) remain the kernel's own here. #### `with_roles_loop_spec` ```lean theorem with_roles_loop_spec (pred : Slice Value) : ∀ (n : Nat) (items items' : alloc.vec.Vec Value) (index : Usize), pred.val.length - index.val = n → translation.with_roles_loop pred items index = ok items' → items'.val = items.val ++ pred.val.drop index.val ``` #### `with_roles_spec` **`with_roles`**: the predicate tuple with the roles appended as its last element. ```lean theorem with_roles_spec (pred : Slice Value) (roles : Value) (v : Value) (h : translation.with_roles pred roles = ok v) : ∃ items : alloc.vec.Vec Value, v = .List items ∧ items.val = pred.val ++ [roles] ``` #### `single_spec` ```lean theorem single_spec (item v : Value) (h : translation.single item = ok v) : ∃ items : alloc.vec.Vec Value, v = .List items ∧ items.val = [item] ``` #### `theme_atom_spec` **`theme_atom`**: `pred` with the one role `theme`, applied to one term. ```lean theorem theme_atom_spec (pred : Slice Value) (term : first_order.Term) (f : clause_form.Formula) (h : translation.theme_atom pred term = ok f) : ∃ (p : Value) (ts : alloc.vec.Vec first_order.Term) (items roles : alloc.vec.Vec Value), f = .Atom p ts ∧ ts.val = [term] ∧ p = .List items ∧ items.val = pred.val ++ [.List roles] ∧ roles.val = [.Text "theme"] ``` #### `conjoin_loop_spec` ```lean theorem conjoin_loop_spec (constraints : Slice clause_form.Formula) : ∀ (n : Nat) (parts parts' : alloc.vec.Vec clause_form.Formula) (index : Usize), constraints.val.length - index.val = n → translation.conjoin_loop constraints parts index = ok parts' → parts'.val = parts.val ++ constraints.val.drop index.val ``` #### `conjoin_spec` **`conjoin`**: the main formula alone, or one conjunction of it with its constraints. ```lean theorem conjoin_spec (main : clause_form.Formula) (constraints : Slice clause_form.Formula) (f : clause_form.Formula) (h : translation.conjoin main constraints = ok f) : (constraints.val = [] ∧ f = main) ∨ (constraints.val ≠ [] ∧ ∃ parts : alloc.vec.Vec clause_form.Formula, f = .And parts ∧ parts.val = main :: constraints.val) ``` #### `qualified_by_clause_type_spec` **`qualified_by_clause_type`**: a declarative clause (or one with no clause type) is itself; any other clause type wraps the formula as one qualified proposition of that kind, with no bound variable and no cardinality. ```lean theorem qualified_by_clause_type_spec (self : translation.Translator) (key : Str) (result f : clause_form.Formula) (h : translation.Translator.qualified_by_clause_type self key result = ok f) : ∃ o : Option String, translation.Translator.clause_type self key = ok o ∧ ((o = none ∨ o = some "declarative") → f = result) ∧ (∀ kind, o = some kind → kind ≠ "declarative" → ∃ (formulas : alloc.vec.Vec clause_form.Formula) (ks : Str) (empty : Slice first_order.Term), formulas.val = [result] ∧ strOf kind = ok ks ∧ empty.val = [] ∧ translation.qualify (alloc.vec.Vec.deref formulas) ks none empty = ok f) ``` #### `verb_atom_spec` The arguments of a verb, translated one after another: for each `(role, key)` pair the role as a value and the key's term, from the translator state the previous argument left. -/ inductive ArgChain (env : TEnv) (fuel : U32) : translation.Translator → List (String × String) → List Value → List first_order.Term → translation.Translator → Prop | nil (t : translation.Translator) : ArgChain env fuel t [] [] [] t | cons (t t1 t2 : translation.Translator) (role key : String) (ks : Str) (term : first_order.Term) (rest : List (String × String)) (roles : List Value) (terms : List first_order.Term) : strOf key = ok ks → translation.Translator.term t ks env fuel = ok (.Ok term, t1) → ArgChain env fuel t1 rest roles terms t2 → ArgChain env fuel t ((role, key) :: rest) (.Text role :: roles) (term :: terms) t2 theorem verb_atom_loop_failure (self : translation.Translator) (arguments : Slice (String × String)) (env : TEnv) (fuel : U32) (roles : alloc.vec.Vec Value) (terms : alloc.vec.Vec first_order.Term) (e : schema_tree.TreeError) (index : Usize) (out : translation.Translator × alloc.vec.Vec Value × alloc.vec.Vec first_order.Term × Option schema_tree.TreeError) (h : translation.Translator.verb_atom_loop self arguments env fuel roles terms (some e) index = ok out) : out.2.2.2 = some e := by unfold translation.Translator.verb_atom_loop at h dsimp only at h split at h · simp only [core.option.Option.is_none] at h split at h · rename_i hb exact absurd hb (by simp) · rw [ok_eq_ok_iff] at h rw [← h] · rw [ok_eq_ok_iff] at h rw [← h] theorem verb_atom_loop_spec (arguments : Slice (String × String)) (env : TEnv) (fuel : U32) : ∀ (n : Nat) (self self' : translation.Translator) (roles roles' : alloc.vec.Vec Value) (terms terms' : alloc.vec.Vec first_order.Term) (index : Usize), arguments.val.length - index.val = n → translation.Translator.verb_atom_loop self arguments env fuel roles terms none index = ok (self', roles', terms', none) → ∃ rs ts, roles'.val = roles.val ++ rs ∧ terms'.val = terms.val ++ ts ∧ ArgChain env fuel self (arguments.val.drop index.val) rs ts self' := by intro n induction n with | zero => intro self self' roles roles' terms terms' index hk h unfold translation.Translator.verb_atom_loop at h dsimp only at h have hlen : arguments.length = arguments.val.length := rfl have hlen' := Slice.len_val arguments split at h · exfalso rename_i hlt scalar_tac · rw [ok_eq_ok_iff] at h simp only [Prod.mk.injEq] at h obtain ⟨hs, hr, ht, _⟩ := h subst hs hr ht refine ⟨[], [], by simp, by simp, ?_⟩ rw [List.drop_of_length_le (by omega)] exact ArgChain.nil _ | succ n ih => intro self self' roles roles' terms terms' index hk h unfold translation.Translator.verb_atom_loop at h dsimp only at h have hlen : arguments.length = arguments.val.length := rfl have hlen' := Slice.len_val arguments split at h · rename_i hlt rw [if_pos (show core.option.Option.is_none (none : Option schema_tree.TreeError) = true from rfl)] at h read_ok at h obtain ⟨p, hp, q, hq, failure1, hfail, h⟩ := h obtain ⟨r, self1, roles1, terms1⟩ := q dsimp only at hq hfail h have hp' := slice_index_usize_eq_ok _ _ _ hp have hlt' : index.val < arguments.val.length := by scalar_tac have hidx : (core.num.Usize.wrapping_add index 1#usize).val = index.val + 1 := usize_succ_val index arguments.val.length hlt' arguments.property -- one argument unfold translation.Translator.push_argument alloc.string.String.Insts.CoreOpsDerefDerefStr.deref at hq obtain ⟨role, key⟩ := p try dsimp only at hq read_ok at hq obtain ⟨s2, hs2, v, hv, roles2, hroles2, s3, hs3, q2, hq2, cf, hcf, hq⟩ := hq obtain ⟨r2, self2⟩ := q2 dsimp only at hq2 hcf hq obtain ⟨roleS, hroleS, hv'⟩ := s_spec _ _ hv rw [decodeUtf8_strOf _ _ hs2] at hroleS have hroleS' := Option.some.inj hroleS subst hroleS' hv' cases r2 with | Err e => simp only [core.result.Result.Insts.CoreOpsTry.branch, ok_eq_ok_iff] at hcf subst hcf dsimp only at hq read_ok at hq obtain ⟨r3, hr3, hq⟩ := hq obtain ⟨e', he'⟩ := from_residual_is_err _ _ _ hr3 subst he' simp only [ok_eq_ok_iff, Prod.mk.injEq] at hq obtain ⟨hr, _, _, _⟩ := hq subst hr dsimp only at hfail rw [ok_eq_ok_iff] at hfail subst hfail exfalso have := verb_atom_loop_failure _ _ _ _ _ _ _ _ _ h simp at this | Ok term => simp only [core.result.Result.Insts.CoreOpsTry.branch, ok_eq_ok_iff] at hcf subst hcf dsimp only at hq read_ok at hq obtain ⟨terms2, hterms2, hq⟩ := hq simp only [ok_eq_ok_iff, Prod.mk.injEq] at hq obtain ⟨hr, hself, hroles, hterms⟩ := hq subst hr hself hroles hterms dsimp only at hfail rw [ok_eq_ok_iff] at hfail subst hfail obtain ⟨rs, ts, hroles', hterms', hchain⟩ := ih self2 self' roles2 roles' terms2 terms' _ (by omega) h refine ⟨.Text role :: rs, term :: ts, ?_, ?_, ?_⟩ · rw [hroles', vec_push_eq_ok _ _ _ hroles2] simp · rw [hterms', vec_push_eq_ok _ _ _ hterms2] simp · have hdrop : arguments.val.drop index.val = (role, key) :: arguments.val.drop (index.val + 1) := by rw [List.drop_eq_getElem_cons hlt'] rw [(List.getElem?_eq_some_iff.mp hp').2] rw [hdrop] rw [hidx] at hchain exact ArgChain.cons self self2 self' role key s3 term _ rs ts hs3 hq2 hchain · exfalso rename_i hge scalar_tac /-- **`verb_atom`** (§4.3): the predicate with its arguments' roles appended, applied to the arguments' terms, both in the order of the argument pairs. ```lean theorem verb_atom_spec (self self' : translation.Translator) (pred : Slice Value) (arguments : Slice (String × String)) (env : TEnv) (fuel : U32) (f : clause_form.Formula) (h : translation.Translator.verb_atom self pred arguments env fuel = ok (.Ok f, self')) : ∃ (p : Value) (ts : alloc.vec.Vec first_order.Term) (items roles : alloc.vec.Vec Value), f = .Atom p ts ∧ p = .List items ∧ items.val = pred.val ++ [.List roles] ∧ ArgChain env fuel self arguments.val roles.val ts.val self' ``` #### `nonverbal_atom_spec` **`nonverbal_atom`** (§4.3): the occurrence is predicated of its subject, or of itself when it has none; its atom is the full predicate when it is not a noun or when the predicate is its own description, the description alone when it is only described, and both conjoined when a described noun is predicated. The subject's term is the kernel's `term` for the subject key (the occurrence itself when unpredicated), and the translator state is the one that term left. ```lean theorem nonverbal_atom_spec (self self' : translation.Translator) (key pos : Str) (subject : Option String) (pred description : Slice Value) (env : TEnv) (fuel : U32) (f : clause_form.Formula) (h : translation.Translator.nonverbal_atom self key pos subject pred description env fuel = ok (.Ok f, self')) : ∃ (subjectS : String) (sk : Str) (term : first_order.Term) (same : Bool), (subject = none → decodeUtf8 key.val = some subjectS) ∧ (∀ s, subject = some s → subjectS = s) ∧ strOf subjectS = ok sk ∧ translation.Translator.term self sk env fuel = ok (.Ok term, self') ∧ core.slice.cmp.PartialEqSlice.eq canonical_value.Value.Insts.CoreCmpPartialEqValue description pred = ok same ∧ (decodeUtf8 pos.val ≠ some "N" → translation.theme_atom pred term = ok f) ∧ (decodeUtf8 pos.val = some "N" → (subject.isSome = true → same = true → translation.theme_atom pred term = ok f) ∧ (subject = none → translation.theme_atom description term = ok f) ∧ (subject.isSome = true → same = false → ∃ (a b : clause_form.Formula) (parts : alloc.vec.Vec clause_form.Formula), translation.theme_atom pred term = ok a ∧ translation.theme_atom description term = ok b ∧ f = .And parts ∧ parts.val = [a, b])) ``` #### `atom_lexical` **A lexical occurrence's atom** (§4.3), when it is not a copula: its main atom is the verb atom (a verb) or the nonverbal atom (a noun or adjective) over the predicate `predicates_for` gives it; its constraints are every edge's and every possession's; the result is the main atom conjoined with the constraints and wrapped by the clause type. The predicate tuples, the edges an atom reads and the constraints' contents are the kernel's own here. ```lean theorem atom_lexical (self self' : translation.Translator) (key : Str) (env : TEnv) (claim_of host of : Str) (fuel : U32) (φ : clause_form.Formula) (n : working_graph.GNode) (h : translation.Translator.atom self key env claim_of host of fuel = ok (.Ok φ, self')) (hnode : translation.Translator.node self key = ok (.Ok n)) (hkind : n.kind ≠ .Combinator) (hcopula : sorted_collections.Map.contains_key alloc.string.String.Insts.CoreCmpOrd Str.Insts.CoreCmpOrd alloc.string.String.Insts.CoreBorrowBorrowStr self.copulas key = ok false) : ∃ (f : U32) (subject : Option String) (posS : Str) (is_verb : Bool) (edges : alloc.vec.Vec (Option String × String)) (arguments : alloc.vec.Vec (String × String)) (pred description : alloc.vec.Vec Value) (main : clause_form.Formula) (self1 self2 self3 : translation.Translator) (constraints constraints1 : alloc.vec.Vec clause_form.Formula) (f1 : clause_form.Formula), U32.checked_sub fuel 1#u32 = some f ∧ translation.Translator.subject_for self key of = ok subject ∧ strOf n.pos = ok posS ∧ (is_verb = true ↔ n.pos = "V") ∧ translation.Translator.atom_edges self key (decide (n.pos = "N")) subject host = ok edges ∧ translation.Translator.argument_pairs self key (alloc.vec.Vec.deref edges) = ok arguments ∧ translation.Translator.predicates_for self key (alloc.vec.Vec.deref edges) claim_of host f = ok (.Ok (pred, description)) ∧ (is_verb = true → translation.Translator.verb_atom self (alloc.vec.Vec.deref pred) (alloc.vec.Vec.deref arguments) env f = ok (.Ok main, self1)) ∧ (is_verb = false → translation.Translator.nonverbal_atom self key posS subject (alloc.vec.Vec.deref pred) (alloc.vec.Vec.deref description) env f = ok (.Ok main, self1)) ∧ translation.Translator.all_edge_constraints self1 key is_verb (alloc.vec.Vec.deref edges) env f (alloc.vec.Vec.new clause_form.Formula) = ok (.Ok (), self2, constraints) ∧ translation.Translator.possession_constraints self2 key (alloc.vec.Vec.deref arguments) env f constraints = ok (.Ok (), self3, constraints1) ∧ translation.conjoin main (alloc.vec.Vec.deref constraints1) = ok f1 ∧ translation.Translator.qualified_by_clause_type self3 key f1 = ok φ ∧ self' = self3 ``` 28:I[485605,["$1","$2","$3","$4","$5","$6","$7","$8"],"OutletBoundary"] 18:[["children",{"s":"__PAGE__","h":512,"d":{"r":["$","$b","c",{"children":[["$","$L1a",null,{"markdown":"$1b"}],["$L1c"],"$L1d"]}],"p":false,"v":null}}]] 16:[["children",{"s":"docs","h":512,"d":{"r":["$","$b","c",{"children":[null,["$","$L12",null,{"parallelRouterKey":"children","error":"$undefined","errorStyles":"$undefined","errorScripts":"$undefined","template":["$","$L15",null,{}],"templateStyles":"$undefined","templateScripts":"$undefined","notFound":"$undefined","forbidden":"$undefined","unauthorized":"$undefined"}]]}],"p":false,"v":"$17"},"c":"$Q18"}]]