Lax58.CertifiedDerivation
Field-encoding agreement (infrastructure)
concepts/Lax58/CertifiedDerivation.lean · lax-58
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Infrastructure
An agreement witness fixes an encoder and a proposition, supplies an implementation equal to that encoder, and carries a proof of the proposition. The operations below retain natural values, erase subtype proofs, and enumerate finite families in intrinsic order.
This record is bookkeeping for generated certificates, not a standalone definition of advice-freedom: an arbitrary encoder and an arbitrary true proposition can have an agreement witness. The constructor equations generated for a particular datatype supply the semantic specification.
Use for the closed derivation command. Its field resolver accepts only approved primitives and previously generated datatype witnesses, never arbitrary values of this record. Constructor privacy alone is not a proof boundary; the indexed specification and equality obligation prevent replacing a specified encoder with a different function.
Lean source view on GitHub
| 1 | import Lax58.StructuralCombinators |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Field-encoding agreement (infrastructure) |
| 6 | type: infrastructure |
| 7 | --- |
| 8 | |
| 9 | An agreement witness fixes an encoder and a proposition, supplies an |
| 10 | implementation equal to that encoder, and carries a proof of the proposition. |
| 11 | The operations below retain natural values, erase subtype proofs, and |
| 12 | enumerate finite families in intrinsic order. |
| 13 | |
| 14 | This record is bookkeeping for generated certificates, not a standalone |
| 15 | definition of advice-freedom: an arbitrary encoder and an arbitrary true |
| 16 | proposition can have an agreement witness. The constructor equations generated |
| 17 | for a particular datatype supply the semantic specification. |
| 18 | |
| 19 | Use `Lax58.CertifiedDerivationElab` for the closed derivation command. Its |
| 20 | field resolver accepts only approved primitives and previously generated |
| 21 | datatype witnesses, never arbitrary values of this record. Constructor |
| 22 | privacy alone is not a proof boundary; the indexed specification and equality |
| 23 | obligation prevent replacing a specified encoder with a different function. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax58.CertifiedDerivation |
| 27 | |
| 28 | open Lax58.StructuralPresentation Lax58.StructuralCombinators |
| 29 | |
| 30 | universe u |
| 31 | |
| 32 | /-- A checked implementation of a specified canonical encoder and law. |
| 33 | Both specifications are type indices, so even tactics accessing the private |
| 34 | constructor cannot replace them. Provenance of the specifications comes from |
| 35 | the closed derivation command, which never accepts arbitrary witness values. -/ |
| 36 | structure CertifiedFieldEncoding (α : Type u) (canonical : α → Raw) (laws : Prop) where |
| 37 | private mk :: |
| 38 | toRaw : α → Raw |
| 39 | agrees : toRaw = canonical |
| 40 | checked : laws |
| 41 | |
| 42 | namespace CertifiedFieldEncoding |
| 43 | |
| 44 | /-- Package a specified encoder with a proof of its law. This constructs only |
| 45 | an agreement value: it does not register a datatype or certify the provenance |
| 46 | of the supplied specification. The derivation command alone manages that |
| 47 | registry, after inspecting the source constructors. -/ |
| 48 | def ofLaws {α : Type u} (canonical : α → Raw) {laws : Prop} (checked : laws) : |
| 49 | CertifiedFieldEncoding α canonical laws := |
| 50 | ⟨canonical, rfl, checked⟩ |
| 51 | |
| 52 | /-- The law fixed by a certificate's type, not chosen by its implementation. -/ |
| 53 | def Laws {α : Type u} {canonical : α → Raw} {laws : Prop} |
| 54 | (_P : CertifiedFieldEncoding α canonical laws) : Prop := laws |
| 55 | |
| 56 | /-- The natural-number primitive. -/ |
| 57 | def nat : CertifiedFieldEncoding Nat Raw.nat (∀ n : Nat, Raw.nat n = Raw.nat n) := |
| 58 | ⟨Raw.nat, rfl, fun _ => rfl⟩ |
| 59 | |
| 60 | /-- Finite indices retain their natural value. -/ |
| 61 | def fin (n : Nat) : CertifiedFieldEncoding (Fin n) (fun i => Raw.nat i.val) |
| 62 | (∀ i : Fin n, Raw.nat i.val = Raw.nat i.val) := |
| 63 | ⟨fun i => Raw.nat i.val, rfl, fun _ => rfl⟩ |
| 64 | |
| 65 | /-- Erase only a subtype's proof, retaining its certified computational field. -/ |
| 66 | def subtype {α : Type u} {canonical : α → Raw} {laws : Prop} |
| 67 | (P : CertifiedFieldEncoding α canonical laws) (p : α → Prop) : |
| 68 | CertifiedFieldEncoding (Subtype p) (fun x => canonical x.val) laws := |
| 69 | ⟨fun x => canonical x.val, rfl, P.checked⟩ |
| 70 | |
| 71 | /-- Enumerate a possibly dependent finite family in intrinsic index order. -/ |
| 72 | def family {n : Nat} {α : Fin n → Type u} |
| 73 | {canonical : (i : Fin n) → α i → Raw} {laws : Fin n → Prop} |
| 74 | (P : (i : Fin n) → CertifiedFieldEncoding (α i) (canonical i) (laws i)) : |
| 75 | CertifiedFieldEncoding ((i : Fin n) → α i) |
| 76 | (fun f => Raw.fields (List.ofFn fun i => canonical i (f i))) (∀ i, laws i) := |
| 77 | ⟨fun f => Raw.fields (List.ofFn fun i => canonical i (f i)), |
| 78 | rfl, fun i => (P i).checked⟩ |
| 79 | |
| 80 | end CertifiedFieldEncoding |
| 81 | |
| 82 | end Lax58.CertifiedDerivation |
| 83 |
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments