Documentation

Transfer.Hierarchy.ParamWeaken

The ⊑-driven Param weakening (level navigation) #

ParamLevel.lean supplies the MapClass lattice order ⊑ and the meet. This module supplies the witness-level counterpart: the function that turns a synthesized witness at a level into a witness at any lower level the lattice order permits. This is the mechanism behind "synthesize at the strongest available level, then use at the minimal level a goal needs" — the downward (forget) half of the level navigation.

The crux is forgetMapHas: for any m' ⊑ m, a MapHas m R forgets down to a MapHas m' R, by composing the per-level forgets already proved in ParamHierarchy.lean (Map4Has.toMap3, Map3Has.toMap2a/toMap2b, Map2aHas.toMap1/Map2bHas.toMap1, Map1Has.forget). It is a full case enumeration on the target m' then the source m; the lattice-invalid pairs are discharged from the hypothesis h : m' ⊑ m, which reduces to false = true there.

Param.weaken then forgets both directions (forward on fwd, backward on bwd), giving the lattice's action on annotated relations:

a witness at (m, n) supplies a witness at every (m', n') with m' ⊑ m and n' ⊑ n.

This completes the lattice navigation: meet (the least common level, ParamLevel) plus forgetMapHas/Param.weaken (forget down to it). The remaining piece of the level solver is the upward search — picking which level to synthesize at, i.e. a MetaM/outParam resolver that reads the arrowReq/forallReq decision tables (ParamLevel.lean) to choose the combinator and the minimal feasible level before invoking the synthesizer. That resolver, resolveParamLevel, is the final step; Param.weaken lets it synthesize high and land at the lower level a goal uses.

forgetMapHas — forget one direction down the lattice #

source
def Transfer.Param.forgetMapHas {A B : Type u} {R : A → B → Prop} (m' m : MapClass) :
(fun (a b : MapClass) => a.le b = true) m' m → MapHas m R → MapHas m' R

Forget down the lattice (one direction). For m' ⊑ m, downgrade a MapHas m R to a MapHas m' R by composing the per-level forgets from ParamHierarchy.lean. Full case enumeration on the target m' then the source m; lattice-invalid pairs (m' ⊑ m is false) are discharged from h : m' ⊑ m, whose type reduces to false = true.

Equations
Instances For

    Param.weaken — the lattice action on annotated relations #

    source
    def Transfer.Param.Param.weaken {m m' n n' : MapClass} {A B : Type u} (hm : m'.le m = true) (hn : n'.le n = true) (p : Param m n A B) :
    Param m' n' A B

    Weaken an annotated relation down the lattice. Given m' ⊑ m and n' ⊑ n, a Param m n A B forgets to a Param m' n' A B: keep the relation R, forget the forward witness fwd to level m' and the backward witness bwd to level n'. This is the "synthesize-high, use-low" move: the synthesizer may produce at the strongest available level, and Param.weaken brings it to the minimal level the goal needs.

    Equations
    Instances For

      Examples — exercising the weakening on the concrete witnesses #

      paramOfEmbedding : Param map3 map0 (graph of an encoder, no decoder) and paramOfEquiv : Param map3 map2b (left-inverse encoding) are the two concrete Param constructors in the hierarchy. Every weakening below is a one-liner Param.weaken (by decide) (by decide) _.

      source
      def Transfer.Param.embeddingAsMap1 {A α : Type u} [ReprEmbeddingClass A α] :
      Param MapClass.map1 MapClass.map0 A α

      paramOfEmbedding : Param map3 map0 weakens to Param map1 map0 (forward forgets map3 → map1; backward stays map0).

      Equations
      Instances For
        source
        def Transfer.Param.embeddingAsMap2a {A α : Type u} [ReprEmbeddingClass A α] :
        Param MapClass.map2a MapClass.map0 A α

        paramOfEmbedding : Param map3 map0 weakens to Param map2a map0 (forward forgets map3 → map2a, the map-with-graph-inclusion).

        Equations
        Instances For
          source
          def Transfer.Param.equivAsMap0Map2b {A α : Type u} [ReprEquivClass A α] :
          Param MapClass.map0 MapClass.map2b A α

          paramOfEquiv : Param map3 map2b weakens to Param map0 map2b (forward forgets all the way to map0; backward stays map2b).

          Equations
          Instances For
            source
            def Transfer.Param.equivAsMap1Map0 {A α : Type u} [ReprEquivClass A α] :
            Param MapClass.map1 MapClass.map0 A α

            paramOfEquiv : Param map3 map2b weakens to Param map1 map0 (forward map3 → map1; backward map2b → map0).

            Equations
            Instances For

              Tie to the minimal-level solver #

              The general "synthesize-high, use-low" statement: any witness at (m, n) supplies one at every lattice-lower target (m', n'). A level resolver thus synthesizes at the strongest level available and applies Param.weaken to land at the minimal level a goal requires; the ⊑ premises are decidable (MapClass.le is Bool-valued), so each landing is a by decide.

              source
              theorem Transfer.Param.weaken_lands_below {m m' n n' : MapClass} {A B : Type u} (hm : m'.le m = true) (hn : n'.le n = true) (p : Param m n A B) :
              Nonempty (Param m' n' A B)

              Synthesize-high, use-low. Given a witness at (m, n) and any target (m', n') lattice-below it, Param.weaken supplies the target witness. This is the downward half of the level solver.