substitution within Sigma

Stream: new members

[Simon Jacobsson]

Hello,
I am having some trouble with making a substitution inside a dependent product.

Here is the context:
I defined natural numbers as a type mynat by assuming their UP as axioms, and from that I want to show that inductive definitions are legal. So I have written down a theorem

variables (AA : Type) (A : set AA) (n : mynat)

 theorem inductive_definitions_general
   (g : (Σ n : mynat, minus n -> A) -> A) :
   ∃! (f : mynat -> A),
     forall m : mynat,
       f m = g ⟨m, (minus m).restrict f⟩

where minus n is the set of naturals ≤ n.

Here is the problem:
In the base case of my induction, I have the following state,

g : (Σ (n : mynat), ↥(minus n) → ↥A) → ↥A
m : mynat
h_m : m = zero
minus_zero : minus zero = set.empty
⊢ ?m_1 m = g ⟨ m, (minus m).restrict ?m_1 ⟩

and I want to make the substitutions

rw h_m,
rw minus_zero,

but I get the error motive is not type correct. I looked at some Zulip threads about other people who have had this problem, especially this one, and it seems in general that people resolve the problem by changing rw to simp_rw or subst but I have tried that and it does not work. My questions are basically

1. if it makes sense to expect to be able to make an arbitrary substitution inside a dependent type like this
2. and if so, what am I doing wrong?

[Eric Wieser]

I feel like things may have already gone wrong by the time the ?m_1 appears; can you give a #mwe that shows how you got there?

[Simon Jacobsson]

Okay, I just have to get it to compile :sweat_smile:

[Simon Jacobsson]

Okay, sorry if not very minimal, but here it is:

import data.set
import data.set.function

axiom mynat : Type
axiom zero : mynat
axiom succ : mynat -> mynat
axiom succ_neq_0 {a : mynat} : not (succ a = zero)
axiom succ_sur {a : mynat} : not (a = zero) -> exists b : mynat, succ b = a
axiom succ_inj : function.injective succ
axiom myinduction {A : set mynat} : zero ∈ A -> (forall n : mynat, n ∈ A -> succ n ∈ A) -> A = set.univ

def Inter {T} (AA : set (set T)) : set T := {t : T | forall A ∈ AA, t ∈ A}
def final (A : set mynat) : Prop :=
  and
    (A.nonempty)
    (forall n : mynat, n ∈ A -> succ n ∈ A)
def plus (n : mynat) : set mynat :=
  Inter {F | and (n ∈ F) (final F)}
def minus (n : mynat) : set mynat :=
  compl $ plus n

def leq (m n : mynat) : Prop := minus m ⊆ minus n
infix `≤`:80 := leq

lemma leq_zero {n : mynat} : (n ≤ zero) <-> n = zero :=
begin sorry, end

lemma minus_zero : minus zero = ∅ :=
begin sorry, end

variables {AA : Type} {A : set AA}
variable {n : mynat}

theorem inductive_definitions_general
  (g : (Σ n : mynat, minus n -> A) -> A) :
  ∃! (f : mynat -> A),
    forall m : mynat,
      f m = g ⟨m, (minus m).restrict f⟩
  :=
begin
  apply exists_unique.intro,

    let I := {n : mynat | exists (h : mynat -> A), forall m ≤ n, h m = g ⟨m, (minus m).restrict h⟩},
    have h_I : I = set.univ,
    apply myinduction,
      simp,

      split,
        intros m h_m,
        rw leq_zero at h_m,
        rw h_m,
        rw minus_zero,
end

[Simon Jacobsson]

The block

let I := {n : mynat | exists (h : mynat -> A), forall m ≤ n, h m = g ⟨m, (minus m).restrict h⟩},
have h_I : I = set.univ,
apply myinduction,

in the proof of the theorem is basically synonymous with the induction tactic.

[Eric Wieser]

What was your intent with apply exists_unique.intro?

[Eric Wieser]

That says "I'm going to provide you a witness, but I'm not going to tell you what it is yet

[Eric Wieser]

What's the witness you want to use?

[Simon Jacobsson]

Eric Wieser said:

What was your intent with apply exists_unique.intro?

Okay maybe that's the problem then, because I just wanted to split the ∃! into "existence" and "uniqueness".

[Eric Wieser]

For that you need docs#exists_unique_of_exists_of_unique

[Simon Jacobsson]

Eric Wieser said:

What's the witness you want to use?

Since I am planning to use my induction axiom I guess I am not going to provide a witness.

[Eric Wieser]

But that might be harder to prove, because then you have to prove "there exists an x such that p x, and if p y and p z then y = z", rather than the likely easier "there exists an x such that p x, and if p ythen x = y"

[Eric Wieser]

Either way, if splitting into "existence" and "uniqueness" is what your pen and paper proof does, then I recommend going ahead with exists_unique_of_exists_of_unique

[Simon Jacobsson]

I will test it out,
Thanks for the input! :)

[Simon Jacobsson]

Hmmm, I still get the same error even when I try exists_unique_of_exists_of_unique.
I also tried getting rid of the split:

begin
  apply exists_unique_of_exists_of_unique,

    let I := {n : mynat | exists (h : mynat -> A), forall m ≤ n, h m = g ⟨m, (minus m).restrict h⟩},
    have h_I : I = set.univ,
    apply myinduction,
      simp,

      have h_ : mynat -> A, sorry,
      simp [leq_zero],
      use (fun _, g ⟨zero, (minus zero).restrict h_⟩),
      rw minus_zero,

end

but still get the same error...

[Simon Jacobsson]

I assumed that I have some arbitrary function into A (I guess strictly speaking I should assume that A is nonempty) because once I manage to substitute away minus zero, h_ does not matter since its restriction is just the empty function.

[Eric Wieser]

This makes progress:

      congr' 2,
      ext x,
      dsimp,
      rw minus_zero at x,  -- or `have x' := minus_zero.rec x,` and use `x'` below
      exact x.prop.elim,

[Eric Wieser]

The problem is you can't rewrite the minus_zero you're seeing, because g expects an argument of type (Σ n : mynat, minus n -> A), but you're trying to rewrite the minus to not be there any more

[Simon Jacobsson]

Yes, that solves the goal :).
Okay, I will have to look at what congr' and ext does.