Dependent `And`

Stream: lean4

[Mac Malone]

How does one write a dependent And in Lean 4? PSigma is not in Prop and Exists does not permit destructing into non-Prop.

-- tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
example (i : Nat) (a : Array Nat) (law : ∃ h : i < a.size, a.get ⟨i, h⟩ = 0) : Nat :=
  have ⟨lt_size, z_eq⟩ := law
  i

-- has type `Type`, but is expected to have type `Prop`
def law (i : Nat) (a : Array Nat) : Prop := Σ' h : i < a.size, a.get ⟨i, h⟩ = 0

[Arthur Adjedj]

Writing your own PropSigma also gives out a code generation error which, to me, looks like a bug:

inductive PropSigma {P : Prop} (Q : P → Prop) : Prop :=
  | intro : (p : P) → Q p → PropSigma Q

--unsupported `PropSigma.casesOn` application during code generation
example (i : Nat) (a : Array Nat) (law : PropSigma (λ h : i < a.size => a.get ⟨i, h⟩ = 0)) : Nat :=
  have ⟨lt_size, z_eq⟩ := law
  i

edit : nevermind, this behaviour is already documented in the relevant code.

[Junyan Xu]

(deleted)

[Junyan Xu]

With exists you can use

Classical.choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α

and docs#Classical.choose_spec, but I agree when u = 0 (i.e. α : Prop) we should have a version not relying on the axiom of choice.

[Mac Malone]

Another hacky solution is:

inductive PropSigma {P : Prop} (Q : P → Prop) : Prop :=
| intro : (p : P) → ((p : P) → Q p) → PropSigma Q

abbrev PropSigma.fst {Q : P → Prop} : PropSigma Q → P | .intro h _ => h
abbrev PropSigma.snd {Q : P → Prop} : (s : PropSigma Q) → Q s.fst | .intro h f => f h

example (i : Nat) (a : Array Nat) (law : PropSigma (λ h : i < a.size => a.get ⟨i, h⟩ = 0)) : Nat :=
  have lt_size := law.fst
  have z_eq := law.snd
  i

But this removes the ability to use pattern matching syntax for proper destructing.

[Junyan Xu]

Hmm, docs#Exists.fst and docs#Exists.snd are already there! You can even write law.1 law.2.

[Mac Malone]

@Junyan Xu Interesting, so it is just the casesOn eliminator that is broken for this special case.

[Junyan Xu]

I think it's behaving as expected as your goal is Nat : Type not _ : Prop.

[Junyan Xu]

For example these work:

lemma Exists.fst' {b : Prop} {p : b → Prop} (h : ∃ a, p a) : b := have ⟨a, _⟩ := h; a
lemma Exists.snd' {b : Prop} {p : b → Prop} (h : ∃ a, p a) : p h.fst' := have ⟨_, ha⟩ := h; ha

[Mac Malone]

@Junyan Xu Yes, but the problem is there is overlooked case of a dependent and which does need some type (possibly Exists) that properly destructors for it.

[Mac Malone]

However, given that .1 and .2 work for exists, there is the following less hacky solution to the problem:

abbrev Exists.toAnd {b : Prop} {p : b → Prop} (x : Exists p) : And b (p x.1) :=
  ⟨x.1, x.2⟩

-- tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
example (i : Nat) (a : Array Nat) (law : ∃ h : i < a.size, a.get ⟨i, h⟩ = 0) : Nat :=
  have ⟨lt_size, z_eq⟩ := law.toAnd
  i

[Junyan Xu]

I see, apparently casesOn is designed to support more, as this works:

lemma And.fst {a b : Prop} (h : a ∧ b) : ℕ := have ⟨_, _⟩ := h; 0

[Junyan Xu]

I suppose you could also do

have lt_size := law.1; have z_eq := law.2

In Lean 3 it used to be possible to do

obtain ⟨lt_size, z_eq⟩ := ⟨law.1, law.2⟩

in tactic mode.

[Eric Wieser]

Junyan Xu said:

You can even write law.1 law.2.

How does this work?

[Junyan Xu]

I don't know! I think it's Lean 4's new feature and I don't think it work in Lean 3.
Probably related to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/invalid.20kernel.20projection.20error.20error

[Mac Malone]

Eric Wieser said:

Junyan Xu said:

You can even write law.1 law.2.

How does this work?

I believe it is because the projection is treated as a separate function of type law.1 : Exists p -> Prop and thus eliminator with that function is eliminating into Prop which works whereas in the destructing case it is eliminating into the arbitrary return type.

[Mario Carneiro]

Projections are typechecked such that x.1 is valid iff x.casesOn fun a _ => a would be type correct