Pulling Subtype.val inside a for-Loop

Stream: new members

[Johannes Tantow]

Hi!
Suppose I have two functions f1 and f2 as definied below. They behave the same on the value but the properties of the resulting subtype may be different. I don't care about these and only want to prove that there values are equal, which seems intuitively true, but I am struggling to prove that. I can destruct the goal further with congr, but this wants me to show (fun a => p a) = fun a => q a, which doesn't seem true to me. Ideally, I want to pull Subtype.val inside the for loop and then it simplifies, but I am unsure how to do that.

def f1 {α ρ: Type u}[ForIn Id ρ α] (l: ρ)(f: α → α → α) (p: α → Prop) (start: α) (pstart: p start) (f_prev: ∀ (a b:α), p a → p (f a b)): {a: α // p a} := Id.run do
  let mut s := ⟨start, pstart⟩

  for a in l do
    s := ⟨f s.1 a, f_prev s.1 a s.2⟩
  return s

def f2 {α ρ: Type u}[ForIn Id ρ α] (l: ρ)(f: α → α → α) (q: α → Prop) (start: α) (qstart: q start) (f_prev: ∀ (a b:α), q a → q (f a b)): {a: α // q a} := Id.run do
  let mut s := ⟨start, qstart⟩

  for a in l do
    s := ⟨f s.1 a, f_prev s.1 a s.2⟩
  return s

theorem f1_eq_f2_val {α ρ: Type u}[ForIn Id ρ α] (l: ρ)(f: α → α → α) (p: α → Prop) (start: α) (pstart: p start) (f_prev_p: ∀ (a b:α), p a → p (f a b)) (q: α → Prop) (qstart: q start) (f_prev_q: ∀ (a b:α), q a → q (f a b)): (f1 l f p start pstart f_prev_p).1 = (f2 l f q start qstart f_prev_q).1 := by
  unfold f1
  unfold f2
  simp[Id.run]
  admit

Why am I trying to do this? Std.DHashMap.Internal.Raw₀.insertMany has a similar structure and I am trying to prove that the value of it on lists is equal to some function I defined on lists using the constructors of list, so that I can continue with this simpler function to prove results about it. In the induction on lists, I reach such a goal.

[Andrew Yang]

f1_eq_f2_val is false because you have no idea how ForIn is implemented

universe u

def f1 {α ρ : Type u} [ForIn Id ρ α] (l : ρ) (f : α → α → α)
    (p : α → Prop) (start : α) (pstart : p start)
    (f_prev : ∀ a b, p a → p (f a b)) : {a // p a} := Id.run do
  let mut s := ⟨start, pstart⟩

  for a in l do
    s := ⟨f s.1 a, f_prev s.1 a s.2⟩
  return s

def f2 {α ρ : Type u} [ForIn Id ρ α] (l : ρ) (f : α → α → α)
    (q : α → Prop) (start : α) (qstart : q start)
    (f_prev: ∀ a b, q a → q (f a b)) : {a // q a} := Id.run do
  let mut s := ⟨start, qstart⟩

  for a in l do
    s := ⟨f s.1 a, f_prev s.1 a s.2⟩
  return s

theorem f1_eq_f2_val {α ρ : Type u} [ForIn Id ρ α] (l : ρ) (f: α → α → α)
    (p : α → Prop) (start : α) (pstart: p start) (f_prev_p : ∀ (a b:α), p a → p (f a b))
    (q : α → Prop) (qstart : q start) (f_prev_q: ∀ (a b : α), q a → q (f a b)) :
    (f1 l f p start pstart f_prev_p).1 = (f2 l f q start qstart f_prev_q).1 := by
  admit
  -- unfold f1
  -- unfold f2
  -- simp[Id.run]
  -- admit

example : False := by
  classical
  have := @f1_eq_f2_val Nat Nat ⟨fun {β} _ _ d _ ↦
    if e : { n : Nat // True } = β then e.rec ⟨1, trivial⟩ else d⟩ 37 (fun _ _ ↦ 0) (fun _ ↦ True) 0
    trivial (fun _ _ _ ↦ trivial) (· = 0) rfl (fun _ _ _ ↦ rfl)
  have H : { a : Nat // True } ≠ { a // a = 0 } := by
    intro h
    have : Subsingleton { a // a = 0 } := ⟨fun a b ↦ Subtype.ext (a.2.trans b.2.symm)⟩
    have : Subsingleton { a // True } := h ▸ this
    cases this.1 ⟨0, trivial⟩ ⟨1, trivial⟩
  simp [f1, f2, Id.run, H] at this

[Johannes Tantow]

Interesting, thank you. I guess I abstracted a bit too far. For my purpose it would suffice to have that ρ is a List, where your counterexample should no longer work. I try to show the following and at the end I get a similar goal I cannot prove. I hope this time its really true

import Std.Data.DHashMap.Internal.Defs

variable {α : Type u} {β : α → Type v}
namespace Std.DHashMap.Internal.Raw₀

/-- Internal implementation detail of the hash map -/
def insertMany_val [BEq α] [Hashable α]
    (m : Raw₀ α β) (l : List ((a : α) × β a)) : Raw₀ α β := Id.run do
let mut r := m
for ⟨a,b⟩ in l do
  r:= r.insert a b
return r

theorem insertMany_val_eq  [BEq α] [Hashable α]
    (m : Raw₀ α β) (l : List ((a : α) × β a)) : (insertMany m l).val = insertMany_val m l := by
  simp[insertMany, insertMany_val, Id.run]
  induction l generalizing m with
  | nil => simp
  | cons hd tl ih=>
    simp
    specialize ih (m.insert hd.1 hd.2)
    sorry