Zulip Chat Archive
Stream: new members
Topic: How to show definitional equality
Vivek Rajesh Joshi (Jul 02 2024 at 14:59):
import Mathlib.Data.Matrix.Notation
variable (F : Type) [Field F] [DecidableEq F] [Repr F]
abbrev Vector.allZero (v : Vector F n) : Prop := v.toList.all (.=0)
theorem Vector.allZero_def (v : Vector F n) : v.allZero = v.toList.all (.=0) := rfl
instance (v : Vector F n) : Decidable (v.allZero) := inferInstance
structure ReducedRow0 (n : Nat)
structure ReducedRowN0 (n : Nat) where
z : Fin n
k : Nat
tail : Vector F k
h : n = p + k + 1
def ReducedRow (n : Nat) := Sum (ReducedRow0 n) (ReducedRowN0 F n)
def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0
def ReducedRow0.toVector (_ : ReducedRow0 n): Vector F n := zeroVec F n
def ReducedRowN0.toVector (row : ReducedRowN0 F n): Vector F n := row.h ▸ (zeroVec F n).append (Vector.cons 1 row.tail)
def ReducedRow.toVector (row : ReducedRow F n): Vector F n :=
match row with
| .inl row0 => row0.toVector F
| .inr rowN0 => rowN0.toVector F
def ReducedRowN0.zerosAbove (row : ReducedRowN0 F n) (R : Vector (ReducedRowN0 F n) m) : Prop :=
(R.map fun r => (r.toVector F).get row.z).allZero
section
variable (row : ReducedRowN0 F n) (R : Vector (ReducedRowN0 F n) m)
lemma myLemma_1 : ((R.map fun r => (r.toVector F).get row.z).toList.all (.=0)) = row.zerosAbove F R := rfl
instance : Decidable (row.zerosAbove F R) :=
inferInstanceAs <| Decidable ((R.map fun r => (r.toVector F).get row.z).toList.all (.=0))
end
myLemma1
shows that the Decidable instance I want to make is definitionally equal to an already decidable instance. But Lean is not able to make this connection in the instance. How do I force the connection?
Bbbbbbbbba (Jul 02 2024 at 15:37):
This seems to do the trick:
instance t : Decidable (row.zerosAbove F R) :=
inferInstanceAs <| Decidable (((R.map fun r => (r.toVector F).get row.z).toList.all (.=0)) = true)
Vivek Rajesh Joshi (Jul 02 2024 at 16:20):
Thanks!
Last updated: May 02 2025 at 03:31 UTC