dependent elimination failed

Stream: general

[deepest recursion]

hello . is it possible to complete the code below?

import Mathlib
set_option pp.proofs true in
example
  {V:Real}{n1:Int}{r1 : (2:Real) = V}
  {eq1:@HEq { i:Int // n1 = i } ⟨n1, rfl⟩ { i:Int // V = ↑i } ⟨(2:Int), Eq.symm r1⟩ }
: n1 = 2 ∧ (HEq (rfl (a:=n1)) (Eq.symm r1))
:= by
  -- cases eq1
  admit

[Kyle Miller]

I think it's not provable.

There's a model of Lean where { i : Int // n1 = i } and { i : Int // n2 = i } are the same type for all n1 and n2 (this is using the cardinality model: each of these has cardinality one). Proofs have to hold in all models, so that means it's unprovable.

[Violeta Hernández]

Note that the second part of what you want to prove is simply docs#proof_irrel_heq.

[Violeta Hernández]

but yes, HEq often does not behave how you'd wish it did, and if you're using it chances are something went wrong somewhere

[deepest recursion]

is this axiom sound?

#check Sigma.mk.inj_iff

axiom heq_mk_inj_iff {A : Type _} {f h: A → Prop} {a1 a2 : A} {b1 : f a1} {b2 : h a2} :
  (HEq (Subtype.mk a1 b1) (Subtype.mk a2 b2)) = (a1 = a2 ∧ HEq b1 b2)

[suhr]

What do you need this axiom for?

[deepest recursion]

I could use it to complete the example I have given

import Mathlib

axiom heq_mk_inj_iff {A : Type _} {f h: A → Prop} {a1 a2 : A} {b1 : f a1} {b2 : h a2} :
  (HEq (Subtype.mk a1 b1) (Subtype.mk a2 b2)) = (a1 = a2 ∧ HEq b1 b2)

set_option pp.proofs true in
example
  {V:Real}{n1:Int}{r1 : (2:Real) = V}
  {eq1:@HEq { i:Int // n1 = i } ⟨n1, rfl⟩ { i:Int // V = ↑i } ⟨(2:Int), Eq.symm r1⟩ }
: n1 = 2 ∧ (HEq (rfl (a:=n1)) (Eq.symm r1))
:= by
  rw [heq_mk_inj_iff] at eq1
  exact eq1

[Kevin Buzzard]

And why do you want to prove that? Doesn't the cardinality model give a counterexample?

[Kevin Buzzard]

In the cardinality model all singleton types are Eq

[Daniel Weber]

deepest recursion said:

is this axiom sound?

#check Sigma.mk.inj_iff

axiom heq_mk_inj_iff {A : Type _} {f h: A → Prop} {a1 a2 : A} {b1 : f a1} {b2 : h a2} :
  (HEq (Subtype.mk a1 b1) (Subtype.mk a2 b2)) = (a1 = a2 ∧ HEq b1 b2)

Nope

axiom heq_mk_inj_iff {A : Type _} {f h: A → Prop} {a1 a2 : A} {b1 : f a1} {b2 : h a2} :
  (HEq (Subtype.mk a1 b1) (Subtype.mk a2 b2)) = (a1 = a2 ∧ HEq b1 b2)

def f (a : Bool) : Prop := a

def h (_ : Bool) : Prop := True

theorem cast_injective {α β} (h : α = β) {a b} : cast h a = cast h b → a = b := by
  subst h
  exact id

theorem neq : ¬ {a : Bool // h a} = {a : Bool // f a} := by
  intro x
  let a : {a : Bool // h a} := ⟨false, trivial⟩
  let b : {a : Bool // h a} := ⟨true, trivial⟩
  have := cast_injective x (Subtype.ext ((x ▸ a).2.trans (x ▸ b).2.symm))
  simp [a, b] at this

theorem thm : False :=
  neq (heq_mk_inj_iff (f := f) (h := h) (a1 := true) (a2 := true) (b1 := rfl) (b2 := trivial) |>.mpr (by simp [proof_irrel_heq]) |> type_eq_of_heq).symm

#print axioms thm