Nat.Linear.ExprCnstr.denote_toNormPoly
theorem Nat.Linear.ExprCnstr.denote_toNormPoly :
∀ (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr),
Nat.Linear.PolyCnstr.denote ctx c.toNormPoly = Nat.Linear.ExprCnstr.denote ctx c
The theorem `Nat.Linear.ExprCnstr.denote_toNormPoly` states that for any context from the set of natural numbers (`Nat.Linear.Context`) and any expression constraint (`Nat.Linear.ExprCnstr`), the denotation of the normalized polynomial constraint derived from this expression constraint (`Nat.Linear.ExprCnstr.toNormPoly c`) within the given context is equivalent to the denotation of the original expression constraint within the same context (`Nat.Linear.ExprCnstr.denote ctx c`). In simple terms, normalizing an expression constraint does not change its denotation (interpretation) within a given context.
More concisely: The normalization of a natural number expression constraint does not change its denotation within a given context.
|
Nat.Linear.Poly.denote_fuse
theorem Nat.Linear.Poly.denote_fuse :
∀ (ctx : Nat.Linear.Context) (p : Nat.Linear.Poly),
Nat.Linear.Poly.denote ctx p.fuse = Nat.Linear.Poly.denote ctx p
The theorem `Nat.Linear.Poly.denote_fuse` states that for all natural number linear contexts (`ctx`) and all natural number linear polynomials (`p`), the value of the fused polynomial (`Nat.Linear.Poly.fuse p`) evaluated in the context `ctx` (`Nat.Linear.Poly.denote ctx`) is equal to the value of the original polynomial `p` evaluated in the same context. In other words, fusing a polynomial does not change its value in any given context.
More concisely: For all natural number linear contexts `ctx` and polynomials `p`, `Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.fuse p) = Nat.Linear.Poly.denote ctx p`.
|
Nat.Linear.Expr.denote_toPoly
theorem Nat.Linear.Expr.denote_toPoly :
∀ (ctx : Nat.Linear.Context) (e : Nat.Linear.Expr),
Nat.Linear.Poly.denote ctx e.toPoly = Nat.Linear.Expr.denote ctx e
The theorem `Nat.Linear.Expr.denote_toPoly` states that for any given context of natural numbers (`ctx`) and any linear expression (`e`), when we convert this linear expression to a polynomial (`Nat.Linear.Expr.toPoly e`) and then evaluate it (`Nat.Linear.Poly.denote ctx`), the result is equivalent to directly evaluating the original linear expression (`Nat.Linear.Expr.denote ctx e`). In other words, the process of converting a linear expression to a polynomial and evaluating it does not change the outcome as compared to evaluating the original linear expression.
More concisely: For any natural number context `ctx` and linear expression `e`, the conversion of `e` to a polynomial and subsequent evaluation equals the direct evaluation of `e`: `Nat.Linear.Expr.denote ctx (Nat.Linear.Expr.toPoly e) = Nat.Linear.Expr.denote ctx e`.
|
Nat.Linear.Poly.denote_sort_go
theorem Nat.Linear.Poly.denote_sort_go :
∀ (ctx : Nat.Linear.Context) (p r : Nat.Linear.Poly),
Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.sort.go p r) =
Nat.Linear.Poly.denote ctx p + Nat.Linear.Poly.denote ctx r
This theorem states that for any natural number linear context `ctx` and any two natural number linear polynomials `p` and `r`, the denotation (interpretation as a natural number) of the sorted polynomial obtained by the function `sort.go` applied on `p` and `r`, is equal to the sum of the denotations of `p` and `r` in the context `ctx`. In other words, the function `sort.go` preserves the sum operation under the denotation from polynomials to natural numbers.
More concisely: For any natural number linear context `ctx` and natural number linear polynomials `p` and `r`, the denotation of `sort.go (p + r)` equals the denotation of `p` plus the denotation of `r` in context `ctx`.
|
Nat.Linear.ExprCnstr.eq_true_of_isValid
theorem Nat.Linear.ExprCnstr.eq_true_of_isValid :
∀ (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr),
c.toNormPoly.isValid = true → Nat.Linear.ExprCnstr.denote ctx c = True
The theorem `Nat.Linear.ExprCnstr.eq_true_of_isValid` states that for any context `ctx` of type `Nat.Linear.Context` and an expression constraint `c` of type `Nat.Linear.ExprCnstr`, if the polynomial constraint obtained by converting `c` to a normalized polynomial is valid (as determined by the function `Nat.Linear.PolyCnstr.isValid`), then the denotation of the expression constraint `c` in the context `ctx` is true. This essentially means that if the polynomial version of an expression constraint is valid, then the expression constraint itself is also valid or holds true in its context.
More concisely: If a normalized polynomial constraint derived from a Nat.Linear.ExprCnstr in a given context is valid, then the expression constraint holds true in that context.
|