unexpected close of goal with rfl

Stream: new members

[Andre Maute]

Hi there,

I'm experimenting with transporting type classes,

My stripped down example below consists of an equivalence of two data clases 'Square' and 'SquareFin'.

There are structures 'Parent', 'ParenFin', 'Child' and 'ChildFin',
where the 'Child' structures extend the 'Parent' ones.

For the 'Child' class there exists a map 'Child.flip' mapping child to child.
I do NOT want to define 'ChildFin.flip'.

Accordingly to the parallel construction two type classes are defined
'FlippySquare' and 'FlippySquareFin'
both have a property 'is_flippy'.

Question:
Proving 'is_flippy' for an instance of 'FlippySquareFin'
can be done without ever resorting to an 'is_flippy' from 'Child' 'ChildFin' or even 'FlippySquare'
rfl closes the goal, what am I missing here?

I tested my mwe on live.lean-lang.org with the latest Mathlib selected

Best regards
Andre

import Mathlib.Tactic

@[ext]
structure Square (d : Nat) where
  T : Nat → Nat → Nat
  Tinv : Nat → Nat → Nat
  is_T_null_row :
    ∀ k l : Nat,
      k > d
        → T k l = d+1
  is_T_null_col :
    ∀ k l : Nat,
      l > d
        → T k l = d+1
  is_Tinv_null_row :
    ∀ k l : Nat,
      k > d
        → Tinv k l = d+1
  is_Tinv_null_col :
    ∀ k l : Nat,
      l > d
        → Tinv k l = d+1
  is_T_le :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → T k l ≤ d
  is_Tinv_le :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → Tinv k l ≤ d
  is_Tinv_T_id :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → (Tinv k (T k l) = l)
  is_T_Tinv_id :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → (T k (Tinv k l) = l)

@[ext]
structure SquareFin (d : Nat) where
  T : Fin (d + 1) → Equiv.Perm (Fin (d + 1))

def squareEquivPerm (s : Square d) (k : Fin (d + 1)) : Equiv.Perm (Fin (d + 1)) where
  toFun l := by sorry
  invFun l := by sorry
  left_inv := by sorry
  right_inv := by sorry

def SquareEquivSquareFin_toFun (s : Square d)
: SquareFin d where
  T := fun k => squareEquivPerm s k

def SquareEquivSquareFin_invFun (s : SquareFin d)
: Square d where
  T := by sorry
  Tinv := by sorry
  is_T_null_row := by sorry
  is_T_null_col := by sorry
  is_Tinv_null_row := by sorry
  is_Tinv_null_col := by sorry
  is_T_le := by sorry
  is_Tinv_le := by sorry
  is_Tinv_T_id := by sorry
  is_T_Tinv_id := by sorry

theorem SquareEquivSquareFin_right_inv
: ∀ s : SquareFin d,
  SquareEquivSquareFin_toFun (SquareEquivSquareFin_invFun s) = s
:= by sorry

-------

@[ext]
class FlippySquare (d : Nat) (α : Type) where
  T : α → Square d
  flip : α → α
  is_flippy :
    ∀ a : α, ∀ k l : Nat,
      k ≤ d → l ≤ d
      → (T (flip a)).T k l = (T a).T l k

@[ext]
class FlippySquareFin (d : Nat) (α : Type) where
  T : α → SquareFin d
  flip : α → α
  is_flippy :
    ∀ a : α, ∀ k l : Fin (d + 1),
      (T (flip a)).T k l = (T a).T l k

-------

@[ext]
structure Parent (d : Nat) where
  T : Square d

@[ext]
structure ParentFin (d : Nat) where
  T : SquareFin d

-------

def ParentEquivParentFin_toFun (s : Parent d)
: ParentFin d where
  T := SquareEquivSquareFin_toFun s.T

def ParentEquivParentFin_invFun (s : ParentFin d)
: Parent d where
  T := SquareEquivSquareFin_invFun s.T

def ParentEquivParentFin : Parent d ≃ ParentFin d where
  toFun s := ParentEquivParentFin_toFun s
  invFun s := ParentEquivParentFin_invFun s
  left_inv := by sorry
  right_inv := by sorry

-------

@[ext]
structure Child (d : Nat)
extends Parent d where

@[ext]
structure ChildFin (d : Nat)
extends ParentFin d where

def ChildEquivChildFin_toFun (s : Child d)
: ChildFin d where
  T := (ParentEquivParentFin_toFun s.toParent).T

def ChildEquivChildFin_invFun (s : ChildFin d)
 : Child d where
  T := (ParentEquivParentFin_invFun s.toParentFin).T

theorem ChildEquivChildFin_left_inv
: ∀ s : Child d,
  ChildEquivChildFin_invFun (ChildEquivChildFin_toFun s) = s
:= by sorry

theorem ChildEquivChildFin_right_inv
: ∀ s : ChildFin d,
  ChildEquivChildFin_toFun (ChildEquivChildFin_invFun s) = s
:= by sorry

def ChildEquivChildFin
: Child d ≃ ChildFin d where
  toFun s := ChildEquivChildFin_toFun s
  invFun s := ChildEquivChildFin_invFun s
  left_inv := by sorry
  right_inv := by sorry

def Child.flip (a : Child d)
: Child d where
  T := by sorry

--- Child.is_flippy is missing intentionally

instance instFlippyChildFin
: FlippySquareFin d (ChildFin d) where
  T := fun a => SquareEquivSquareFin_toFun ((ChildEquivChildFin_invFun a).T)
  flip := fun a => ChildEquivChildFin_toFun ((ChildEquivChildFin_invFun a).flip)
  is_flippy := by
    refine fun a k l => ?_
    unfold ChildEquivChildFin_toFun
    unfold ChildEquivChildFin_invFun
    unfold ParentEquivParentFin_toFun
    unfold ParentEquivParentFin_invFun
    simp
    ext
    rw [SquareEquivSquareFin_right_inv]
    -- Question: Why does rfl close the goal?
    rfl

[Andre Maute]

FYi.
the rfl is on the last line of the mwe

[Robin Arnez]

Well, both sides reduce to the same sorry in toFun in squareEquivPerm

[Robin Arnez]

Specifically, consider

instance instFlippyChildFin
: FlippySquareFin d (ChildFin d) where
  T := fun a => SquareEquivSquareFin_toFun ((ChildEquivChildFin_invFun a).T)
  flip := fun a => ChildEquivChildFin_toFun ((ChildEquivChildFin_invFun a).flip)
  is_flippy a k l := by
    unfold SquareEquivSquareFin_toFun
    dsimp only -- reduce the { T := ... }.T
    unfold squareEquivPerm
    rewrite [Equiv.coe_fn_mk]

[Andre Maute]

if add some conv whnf combinations before the rfl (a hint from Robin), and prepare that state into a theorem

instance instFlippyChildFin
: FlippySquareFin d (ChildFin d) where
  T := fun a => SquareEquivSquareFin_toFun ((ChildEquivChildFin_invFun a).T)
  flip := fun a => ChildEquivChildFin_toFun ((ChildEquivChildFin_invFun a).flip)
  is_flippy := by
    refine fun a k l => ?_
    unfold ChildEquivChildFin_toFun
    unfold ChildEquivChildFin_invFun
    unfold ParentEquivParentFin_toFun
    unfold ParentEquivParentFin_invFun
    simp
    ext
    rw [SquareEquivSquareFin_right_inv]
    conv => lhs; whnf
    conv => rhs; whnf
    -- Question: Why does rfl close the goal?
    rfl

theorem xxx (a : ChildFin d)
:
  ∀ k l : Fin (d + 1),
 (((SquareEquivSquareFin_toFun  (SquareEquivSquareFin_invFun a.T).flip.T).T k) l).1 =
  (((SquareEquivSquareFin_toFun (SquareEquivSquareFin_invFun a.T)).T l) k).1
:= by sorry

one sees in the web ide that the flip has a problem, because there is no Square.flip def
so my question still applies why does rfl close the goal.

[Robin Arnez]

The main reason is that the first sorry in squareEquivPerm does not depend on s, k or l, so it is the same regardless of which value you provide

[Andre Maute]

I will provide the full implementation for the squareEquivPerm. give me some minutes

[Andre Maute]

I can't provide my full not-stripped-down proof.
But the rfl doesn't close now. But In my not-stripped-down proof it still closes. hmm...

import Mathlib.Tactic

@[ext]
structure Square (d : Nat) where
  T : Nat → Nat → Nat
  Tinv : Nat → Nat → Nat
  is_T_null_row :
    ∀ k l : Nat,
      k > d
        → T k l = d+1
  is_T_null_col :
    ∀ k l : Nat,
      l > d
        → T k l = d+1
  is_Tinv_null_row :
    ∀ k l : Nat,
      k > d
        → Tinv k l = d+1
  is_Tinv_null_col :
    ∀ k l : Nat,
      l > d
        → Tinv k l = d+1
  is_T_le :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → T k l ≤ d
  is_Tinv_le :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → Tinv k l ≤ d
  is_Tinv_T_id :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → (Tinv k (T k l) = l)
  is_T_Tinv_id :
    ∀ k l : Nat,
      k ≤ d → l ≤ d
        → (T k (Tinv k l) = l)

@[ext]
structure SquareFin (d : Nat) where
  T : Fin (d + 1) → Equiv.Perm (Fin (d + 1))

def squareTFin (s : Square d) (k l : Fin (d + 1)) : Fin (d + 1) where
  val := s.T k.val l.val
  isLt := by
    refine Nat.lt_add_one_iff.mpr ?_
    exact s.is_T_le k l k.is_le l.is_le

def squareTinvFin (s : Square d) (k l : Fin (d + 1)) : Fin (d + 1) where
  val := s.Tinv k.val l.val
  isLt := by
    refine Nat.lt_add_one_iff.mpr ?_
    exact s.is_Tinv_le k l k.is_le l.is_le

def squareEquivPerm (s : Square d) (k : Fin (d + 1)) : Equiv.Perm (Fin (d + 1)) where
  toFun l := squareTFin s k l
  invFun l := squareTinvFin s k l
  left_inv := by
    unfold Function.LeftInverse
    intro l
    refine Fin.ext_iff.mpr ?_
    unfold squareTFin
    unfold squareTinvFin
    simp
    refine s.is_Tinv_T_id k.val l.val k.is_le l.is_le
  right_inv := by
    unfold Function.RightInverse
    intro l
    refine Fin.ext_iff.mpr ?_
    unfold squareTinvFin
    unfold squareTFin
    simp
    refine s.is_T_Tinv_id k.val l.val k.is_le l.is_le

def SquareEquivSquareFin_toFun (s : Square d)
: SquareFin d where
  T := fun k => squareEquivPerm s k

def SquareEquivSquareFin_invFun (s : SquareFin d)
: Square d where
  T := by sorry
  Tinv := by sorry
  is_T_null_row := by sorry
  is_T_null_col := by sorry
  is_Tinv_null_row := by sorry
  is_Tinv_null_col := by sorry
  is_T_le := by sorry
  is_Tinv_le := by sorry
  is_Tinv_T_id := by sorry
  is_T_Tinv_id := by sorry

theorem SquareEquivSquareFin_right_inv
: ∀ s : SquareFin d,
  SquareEquivSquareFin_toFun (SquareEquivSquareFin_invFun s) = s
:= by sorry

-------

@[ext]
class FlippySquare (d : Nat) (α : Type) where
  T : α → Square d
  flip : α → α
  is_flippy :
    ∀ a : α, ∀ k l : Nat,
      k ≤ d → l ≤ d
      → (T (flip a)).T k l = (T a).T l k

@[ext]
class FlippySquareFin (d : Nat) (α : Type) where
  T : α → SquareFin d
  flip : α → α
  is_flippy :
    ∀ a : α, ∀ k l : Fin (d + 1),
      (T (flip a)).T k l = (T a).T l k

-------

@[ext]
structure Parent (d : Nat) where
  T : Square d

@[ext]
structure ParentFin (d : Nat) where
  T : SquareFin d

-------

def ParentEquivParentFin_toFun (s : Parent d)
: ParentFin d where
  T := SquareEquivSquareFin_toFun s.T

def ParentEquivParentFin_invFun (s : ParentFin d)
: Parent d where
  T := SquareEquivSquareFin_invFun s.T

def ParentEquivParentFin : Parent d ≃ ParentFin d where
  toFun s := ParentEquivParentFin_toFun s
  invFun s := ParentEquivParentFin_invFun s
  left_inv := by sorry
  right_inv := by sorry

-------

@[ext]
structure Child (d : Nat)
extends Parent d where

@[ext]
structure ChildFin (d : Nat)
extends ParentFin d where

def ChildEquivChildFin_toFun (s : Child d)
: ChildFin d where
  T := (ParentEquivParentFin_toFun s.toParent).T

def ChildEquivChildFin_invFun (s : ChildFin d)
 : Child d where
  T := (ParentEquivParentFin_invFun s.toParentFin).T

theorem ChildEquivChildFin_left_inv
: ∀ s : Child d,
  ChildEquivChildFin_invFun (ChildEquivChildFin_toFun s) = s
:= by sorry

theorem ChildEquivChildFin_right_inv
: ∀ s : ChildFin d,
  ChildEquivChildFin_toFun (ChildEquivChildFin_invFun s) = s
:= by sorry

def ChildEquivChildFin
: Child d ≃ ChildFin d where
  toFun s := ChildEquivChildFin_toFun s
  invFun s := ChildEquivChildFin_invFun s
  left_inv := by sorry
  right_inv := by sorry

def Child.flip (a : Child d)
: Child d where
  T := by sorry

--- Child.is_flippy is missing intentionally

instance instFlippyChildFin
: FlippySquareFin d (ChildFin d) where
  T := fun a => SquareEquivSquareFin_toFun ((ChildEquivChildFin_invFun a).T)
  flip := fun a => ChildEquivChildFin_toFun ((ChildEquivChildFin_invFun a).flip)
  is_flippy := by
    refine fun a k l => ?_
    unfold ChildEquivChildFin_toFun
    unfold ChildEquivChildFin_invFun
    unfold ParentEquivParentFin_toFun
    unfold ParentEquivParentFin_invFun
    simp
    ext
    rw [SquareEquivSquareFin_right_inv]
    -- Question: Why does rfl close the goal?
    -- with the squareEquivPerm implementation rfl doesn't close
    rfl

[Andre Maute]

My not-stripped-down proof looks now good to me.
Essentially it boils down to have implementations for the Child.flip def
using some intermediate def Child.flip_Square

def Child.flip_Square (a :ChildSquare d) : Square (d+1)

which then allows to remove the flip.
I don't need to use a Child.is_flippy theorem here either as thought in the beginning.

The confusion must have come from too much sorries, as Robin pointed out.

Best regards and thank you very much Robin, that helped me a lot
Andre