trouble with Eq.rec_on

Stream: new members

[James G]

Hi all, I'm a software engineer with an interest in formal verification. I'm messing around with some silly types-containing-types stuff and I've run into a coercion problem, here's a restricted test case:

import Mathlib.Data.Fintype.Defs

structure ModelBTreeBase where
  Nil : Type
  Fork : Type
  Node : Type
  Node_def : Node = (Nil ⊕ Fork) -- can't find this equality if I define Node with :=
  fork_left : Fork -> Node -> Prop
  fork_left_unique : ∀ f : Fork, ∃! n : Node, fork_left f n
  -- ...

structure ModelBTreeBaseMorph (b1 : ModelBTreeBase) (b2 : ModelBTreeBase) where
  Nil_map : b1.Nil -> b2.Nil
  Fork_map : b1.Fork -> b2.Fork
  Node_map : b1.Node -> b2.Node := b1.Node_def ▸ b2.Node_def ▸ Sum.map Nil_map Fork_map
  preserves_fork_left : ∀ f : b1.Fork, ∀ c : b1.Node,
    b1.fork_left f c -> b2.fork_left (Fork_map f) (Node_map c)
  -- ...

set_option pp.proofs true

def id_ (t : ModelBTreeBase) : ModelBTreeBaseMorph t t :=
  ⟨ id, id, t.Node_def ▸ Sum.map id id,
    by
      intros f c h
      simp
      _
      /-
        t : ModelBTreeBase
        f : t.Fork
        c : t.Node
        h : t.fork_left f c
        ⊢ t.fork_left f (Eq.rec (motive := fun x h ↦ x → x) id (Eq.symm t.Node_def) c)
      -/
  ⟩

It seems to me that that recursor application should be equal to c but it doesn't seem to be definitionally equal. I'm wondering if there's some magic I can invoke to fix this. Looking forward to chatting with you all :)

[Robin Arnez]

Type equality is almost always bad to deal with. Even if it's a bit more annoying, you'd be probably better off with inlining Node in the structure and making it a definition:

import Mathlib.Data.Fintype.Defs

structure ModelBTreeBase where
  Nil : Type
  Fork : Type
  fork_left : Fork -> Nil ⊕ Fork -> Prop
  fork_left_unique : ∀ f : Fork, ∃! n : Nil ⊕ Fork, fork_left f n
  -- ...

abbrev ModelBTreeBase.Node (self : ModelBTreeBase) : Type := self.Nil ⊕ self.Fork

structure ModelBTreeBaseMorph (b1 : ModelBTreeBase) (b2 : ModelBTreeBase) where
  Nil_map : b1.Nil -> b2.Nil
  Fork_map : b1.Fork -> b2.Fork
  Node_map : b1.Node -> b2.Node := Sum.map Nil_map Fork_map
  preserves_fork_left : ∀ f : b1.Fork, ∀ c : b1.Node,
    b1.fork_left f c -> b2.fork_left (Fork_map f) (Node_map c)
  -- ...

def id_ (t : ModelBTreeBase) : ModelBTreeBaseMorph t t :=
  ⟨id, id, Sum.map id id, by intros; simpa⟩

[James G]

Yeah, I was wondering if that was gonna be the solution. Alright, thanks

[James G]

Is abbrev different from def there?

[Robin Arnez]

The difference between abbrev and def is mostly when a declaration can be unfolded. For example, simp can't see through regular defs which might lead to problems since we've used Nil ⊕ Fork before which then, to simp and others, seem like two distinct things. abbrevs on the other hand, can always be unfolded and are also always eagerly unfolded in definitional equality problems.