synCat Tactics

LiftT Basic Usage

Outline

1. Introduce variables, induct, reduce to derivation problem
2. Apply the tactic
3. Eliminate other goals
4. Prove coherence

Introducing variables, quotient induction, and syn_hom

mkCount

semantics/syntacticCat.lean

  meta def incrLeft : nat × nat → tactic(nat × nat)
    | (o,m) := return (succ o, m)
  meta def incrRight : nat × nat → tactic(nat × nat)
    | (o,m) := return (o, succ m)

semantics/syntacticCat.lean

  meta def mkCount : expr →  tactic (nat × nat)
  | `( Π {_ : _ _eq}, %%newGoal) := mkCount newGoal >>= incrLeft
  | `( Π {_ : _ ⟶ _}, %%newGoal) := mkCount newGoal >>= incrRight
  | _ := return (0,0)

Repeat-assume-induct

Documentation

Repeat-assume-replace

Documentation

semantics/syntacticCat.lean

syn_hom [Der : has_struct_derives Form] : 
      ∀ {φ ψ : Form}, (φ ⊢ ψ) → (syn_obj φ ⟶ syn_obj ψ) 

Applying the tactic and eliminating other goals

Proving coherence

Documentation

Simplified LiftT

semantics/syntacticCat.lean

meta def LiftT (T : tactic unit) : tactic unit :=
  do
    -- Count & print how many objects and morphisms to assume
    (numobjs,nummor) ← mkCount,

    /- Assume objects and morphisms, 
      - use induction to get that every object is of the form ⦃φ⦄ for some φ:Form 
      - use syn_hom_inv to turn every assumed morphism into a derivation -/
    repeat_assume_induct (gen_nameList `φ_ numobjs),
    repeat_assume_replace `synCat.syn_hom_inv (gen_nameList `f_ nummor),

    -- Turn the synCat hom goal to a derivation goal
    applyc `synCat.syn_hom,

    -- Apply the input tactic
    T,
    
    -- Eliminate other goals (first stage of cleanup)
    iterate (
      (applyc `deduction_basic.derive_refl)
      <|> assumption
    ),
  
    -- Prove the coherences
    thin_cat.by_thin

Debugging Usage

1. Introduce variables, induct, reduce to derivation problem
2. Apply the tactic
3. Eliminate other goals
4. Prove coherence

Invocation	Description	Tasks Performed
LiftT	Regular use	1,2,3,4
LiftT?	Just initialize	1
LiftT?!	Tactic application stage	1,2
LiftT?!!	Elimination of other goals	1,2,3