Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Guarded terms

Lax149335.GuardedTerms · concepts/Lax149335/GuardedTerms.lean · lax-149335

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Definition 6.3. Let k∈{1,2,…}k \in \{1, 2, \ldots\}. A term f:A→B∗f : A \to B^* is kk-guarded if it is either

    1. constant: the composition of the unique term A→1A \to 1 with a value; or
    2. long: of the form u⋅h⋅vu \cdot h \cdot v for values u,vu, v of length kk and a simple rational term hh.

    A term f:A→B∗f : A \to B^* is nonempty if it never produces the empty list.

    The reductions of Lemmas 6.4 and 6.5 are about nn-ary co-pairings ⟨f1,…,fn⟩:A1+⋯+An→B∗\langle f_1, \ldots, f_n \rangle : A_1 + \cdots + A_n \to B^* of such terms, and about the nesting depth of the list constructor in a type, on which the proof of Lemma 6.1 is an induction.

    Concept map
    6 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax149335.SimpleRationalWithinSyntax
    2
    3/-!
    4---
    5title: Guarded terms
    6type: definition
    7---
    8**Definition 6.3.** Let k∈{1,2,…}k \in \{1, 2, \ldots\}. A term f:A→B∗f : A \to B^* is *kk-guarded*
    9if it is either
    10
    111. *constant*: the composition of the unique term A→1A \to 1 with a value; or
    122. *long*: of the form u⋅h⋅vu \cdot h \cdot v for values u,vu, v of length kk and a simple
    13 rational term hh.
    14
    15A term f:A→B∗f : A \to B^* is *nonempty* if it never produces the empty list.
    16
    17The reductions of Lemmas 6.4 and 6.5 are about nn-ary co-pairings
    18⟨f1,…,fn⟩:A1+⋯+An→B∗\langle f_1, \ldots, f_n \rangle : A_1 + \cdots + A_n \to B^* of such terms, and about the
    19*nesting depth* of the list constructor in a type, on which the proof of Lemma 6.1 is an
    20induction.
    21
    22# Formalization notes
    23
    24An nn-ary co-pairing, for n≥1n \geq 1, is given by its first term
    25f1:A1→B∗f_1 : A_1 \to B^* and the list of the remaining terms (`Cases`); its input type
    26A1+(A2+⋯+An)A_1 + (A_2 + \cdots + A_n) is `sumTyOf A₁ [A₂, …, Aₙ]`.
    27-/
    28
    29namespace Lax149335.GuardedTerms
    30
    31open Lax149335.Types Lax149335.Terms Lax149335.DerivedTerms Lax149335.DerivedTerms.Term
    32 Lax149335.SimpleRationalWithinSyntax
    33
    34/-- **Definition 6.3.** `f : A → B*` is `k`-guarded if it is constant, or of the form
    35`u · h · v` for values `u`, `v` of length `k` and a simple rational term `h`. -/
    36def KGuarded (k : ℕ) (B : Ty) {A : Ty} (f : Term A B⋆) : Prop :=
    37 (∃ v : Value B⋆, f = toUnit A ⨟ v) ∨
    38 (∃ (u v : Value B⋆) (h : Term A B⋆),
    39 IsSimple B h ∧ valLength u = k ∧ valLength v = k ∧ f = dotR (dotL u h) v)
    40
    41/-- A term with list outputs is nonempty if it never produces the empty list. -/
    42def NonemptyOutput {A B : Ty} (f : Term A B⋆) : Prop := ∀ a : ⟦A⟧, f.den a ≠ []
    43
    44/-- The co-product `A₀ + (A₁ + ⋯ + Aₙ)` of a nonempty list of types. -/
    45def sumTyOf : Ty → List Ty → Ty
    46 | A, [] => A
    47 | A, (A' :: As) => A ⊕' sumTyOf A' As
    48
    49/-- A list of terms `Aᵢ → B`, one for each type in a list of types. -/
    50inductive Cases (B : Ty) : List Ty → Type
    51 /-- The empty list of terms. -/
    52 | nil : Cases B []
    53 /-- One more term. -/
    54 | cons {A : Ty} {As : List Ty} : Term A B → Cases B As → Cases B (A :: As)
    55
    56/-- The `n`-ary co-pairing `⟨f₀, f₁, …, fₙ⟩ : A₀ + (A₁ + ⋯ + Aₙ) → B`. -/
    57def copair {B : Ty} : {A : Ty} → {As : List Ty} → Term A B → Cases B As →
    58 Term (sumTyOf A As) B
    59 | _, [], f, _ => f
    60 | _, _ :: _, f, .cons g rest => Term.either f (copair g rest)
    61
    62/-- A property holds for all terms in a list of terms. -/
    63def Cases.All {B : Ty} (P : (A : Ty) → Term A B → Prop) :
    64 {As : List Ty} → Cases B As → Prop
    65 | [], _ => True
    66 | _ :: _, .cons f rest => P _ f ∧ Cases.All P rest
    67
    68/-- The nesting depth of the list constructor in a type. -/
    69def Ty.listDepth : Ty → ℕ
    70 | .unit => 0
    71 | .prod A B => max (Ty.listDepth A) (Ty.listDepth B)
    72 | .sum A B => max (Ty.listDepth A) (Ty.listDepth B)
    73 | .list A => Ty.listDepth A + 1
    74
    75end Lax149335.GuardedTerms
    76
    Formalization notes

    An nn-ary co-pairing, for n≥1n \geq 1, is given by its first term f1:A1→B∗f_1 : A_1 \to B^* and the list of the remaining terms (CasesCases); its input type A1+(A2+⋯+An)A_1 + (A_2 + \cdots + A_n) is sumTyOfA1[A2,…,An]sumTyOf A₁ [A₂, …, Aₙ].

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…