correct by construction/or a typing relation

Stream: general

[Christopher Upshaw]

So I have been trying to formalize an reversible programing language in lean, and have:

structure ctype := (fst snd : base)

notation x ` ⇔ `:50 y := (ctype.mk x y : ctype)

inductive pie : ctype → Type
  | atomic {c} : atomic c → pie c
  | comp {a b c} : pie (a ⇔ b) → pie (b ⇔ c) → pie (a ⇔ c)
  | add {a b c d} :  pie (a ⇔ b) → pie (c ⇔ d) → pie (a + c ⇔ b + d)
  | mul {a b c d} :  pie (a ⇔ b) → pie (c ⇔ d) → pie (a * c ⇔ b * d)

But there are two problems here, one composition is only associative up to isomorphism, when I would really like it to be strictly associative.
And two, the bigger problem, defining recursive functions is a real pain because the equation compiler doesn't seem to be able to handle the polymorphic recursion.

Should I keep going on my path of trying to define and prove well founded a subexpression relation?
Or should I make a untyped version, and then define a typing relation on raw expressions?

If I do the second I should be able to replace comp with comp' : list pie -> pie -> pie and make comp an append.

[Mario Carneiro]

And two, the bigger problem, defining recursive functions is a real pain because the equation compiler doesn't seem to be able to handle the polymorphic recursion.

Do you have an example of this?

[Mario Carneiro]

I would be inclined to go for the untyped version because it's easier to get the equations you want without dependent typing issues

[Christopher Upshaw]

Sure!

def pie.inv : ∀ {a b}, pie (a ⇔ b) → pie (b ⇔ a)
  | a b (pie.atomic atom) := pie.atomic (atom.inv)
  | a b (f >> g) := g.inv >> f.inv
  | a b (f ⊗ g) := f.inv ⊗ g.inv
  |a b (f ♯ g) := f.inv ♯ g.inv

Gives me the error:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (Σ' {a b : base}, pie {fst := a, snd := b})
    (@psigma.has_well_founded base (λ {a : base}, Σ' {b : base}, pie {fst := a, snd := b})
       (@has_well_founded_of_has_sizeof base base.has_sizeof_inst)
       (λ (a : base),
          @psigma.has_well_founded base (λ {b : base}, pie {fst := a, snd := b})
            (@has_well_founded_of_has_sizeof base base.has_sizeof_inst)
            (λ (a_1 : base),
               @has_well_founded_of_has_sizeof (pie {fst := a, snd := a_1})
                 (pie.has_sizeof_inst {fst := a, snd := a_1}))))
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
default_dec_tac failed
state:
pie.inv : Π (_p : Σ' {a b : base}, pie {fst := a, snd := b}), pie {fst := _p.snd.fst, snd := _p.fst},
__mlocal__fresh_75_215 __mlocal__fresh_75_216 __mlocal__fresh_75_217 __mlocal__fresh_75_218 : base,
f : pie {fst := __mlocal__fresh_75_215, snd := __mlocal__fresh_75_216},
g : pie {fst := __mlocal__fresh_75_217, snd := __mlocal__fresh_75_218}
⊢ psigma.lex (λ (a₁ a₂ : base), a₁.sizeof < a₂.sizeof)
    (λ (a : base),
       psigma.lex (λ (a₁ a₂ : base), a₁.sizeof < a₂.sizeof)
         (λ (a_1 : base) (a₁ a₂ : pie {fst := a, snd := a_1}),
            pie.sizeof {fst := a, snd := a_1} a₁ < pie.sizeof {fst := a, snd := a_1} a₂))
    ⟨__mlocal__fresh_75_217, ⟨__mlocal__fresh_75_218, g⟩⟩
    ⟨. (__mlocal__fresh_75_215 + __mlocal__fresh_75_217),
     ⟨. (__mlocal__fresh_75_216 + __mlocal__fresh_75_218), f♯g⟩⟩

[Mario Carneiro]

You should try pie : base -> base -> Type