Zulip Chat Archive

Stream: lean4

Topic: Misunderstanding of simp

Brandon Brown (May 11 2021 at 03:24):

So if I don't use an inductive type where it automatically creates theorems that make things inconsistent and just define a type like this it would work (be sound)? (found a post from Mario suggesting this). And then I'd somehow introduce my own recursor or something

variable (int : Type)
variable (zero : int)
variable (succ : int → int)
variable (pred : int → int)
variable (eq1 : {a : int} → succ (pred a) = a)

Daniel Selsam (May 11 2021 at 03:30):

Yes, the actual integers with standard zero/succ/pred form a model.

Mario Carneiro (May 11 2021 at 15:08):

@Brandon Brown Lean does not directly support constructing higher inductive types, but in many cases, including this one, you can build higher inductive types by quotienting a regular inductive type by the constraints on the constructors. So in this case we would write this:

inductive int_base : Type
| zero : int_base
| succ : int_base → int_base
| pred : int_base → int_base

inductive int_base.rel : int_base → int_base → Prop
| succ_congr : rel a b → rel (succ a) (succ b)
| pred_congr : rel a b → rel (pred a) (pred b)
| succ_pred : rel (succ (pred a)) a
| pred_succ : rel (pred (succ a)) a

def int := Quot int_base.rel
def int.succ (i : int) : int := i.lift (fun a => Quot.mk _ a.succ)
  fun a b h => Quot.sound (int_base.rel.succ_congr h)
def int.pred (i : int) : int := i.lift (fun a => Quot.mk _ a.pred)
  fun a b h => Quot.sound (int_base.rel.pred_congr h)
theorem int.succ_pred {a : int} : succ (pred a) = a :=
  by induction a using Quot.ind with | _ a =>
    exact Quot.sound int_base.rel.succ_pred
theorem int.pred_succ {a : int} : pred (succ a) = a :=
  by induction a using Quot.ind with | _ a =>
    exact Quot.sound int_base.rel.pred_succ

Brandon Brown (May 11 2021 at 16:17):

Oh that's neat, I think I finally get it; I really appreciate you taking the time to write that clear example of the quotient type, @Mario Carneiro . I still do wonder if Lean4 could be extended to support a kind of higher inductive type since it has extensible syntax. Would it be possible to just write syntax for a custom inductive type where you do something like

inductive int : Type where
| zero : int
| succ : int → int
| pred : int → int
and
| eq1 : {a : int} → succ (pred a) = a
| eq2 : {a : int} → pred (succ a) = a

And it would parse this into a set of variables in a namespace

variable (int : Type)
variable (zero : int)
variable (succ : int → int)
variable (pred : int → int)
variable (eq1 : {a : int} → succ (pred a) = a)
variable (eq2: {a : int} → pred (succ a) = a)

along with a recursor and all the other ancillaries that are needed to make an inductive type? Just wondering out of curiosity. And I have no interest in HoTT I just like that higher inductive types appear to make it easier to do some "synthetic mathematics" i.e. axiomatizing something and proving from there rather than having to keep deriving from simpler types.

Yakov Pechersky (May 11 2021 at 16:21):

If you want to do "synthetic mathematics" you can do the following:

class my_int (s : Type) where
  zero : s
  succ : s → s
  pred : s → s
  eq1 : ∀ {a : s}, succ (pred a) = a
  eq2 : ∀ {a : s}, pred (succ a) = a

François G. Dorais (May 11 2021 at 16:22):

Lean 4 syntax is intended to be easily extensible, so this should be possible. (I struggled with a similar construct some long time ago and gave up... I hope experts will chime in with a solution.) Should the "and" allow for anything other than equalities?

Yakov Pechersky (May 11 2021 at 16:22):

(If I got the lean4 syntax right)

Yakov Pechersky (May 11 2021 at 16:22):

Then you can postulate

variable (s : Type _) [my_int s]

Yakov Pechersky (May 11 2021 at 16:23):

Now, Mario showed above that one can actually construct an actual type that can be shown to have a my_int instance. But not all postulated collections are valid. So whatever higher inductive type you make, you'd have to show that it doesn't imply False

François G. Dorais (May 11 2021 at 16:25):

To be clear from my last message, a "solution" would need to create an inductive and then a quotient, perhaps with some equation lemmas to hide the machinery.

Mario Carneiro (May 11 2021 at 16:27):

Yakov Pechersky said:

Now, Mario showed above that one can actually construct an actual type that can be shown to have a my_int instance. But not all postulated collections are valid. So whatever higher inductive type you make, you'd have to show that it doesn't imply False

This is the main reason that Lean doesn't support HITs. In fact the consistency and even a general schema for sound HITs was an open problem for a long time. There are some reasonable looking HITs that are inconsistent

Mario Carneiro (May 11 2021 at 16:28):

The "in many cases" in my earlier post is doing a lot of work there

Mario Carneiro (May 11 2021 at 16:29):

François G. Dorais said:

(I struggled with a similar construct some long time ago and gave up... I hope experts will chime in with a solution.)

Could you elaborate? What did you want to implement?

Brandon Brown (May 11 2021 at 16:36):

I see. So HITs are actually more work than quotient types. I was just cursorily looking at this paper "THE INTEGERS AS A HIGHER INDUCTIVE TYPE" https://arxiv.org/pdf/2007.00167.pdf and was intrigued but looks like it is actually a quite involved construction. I will stick with quotients.

Mario Carneiro (May 11 2021 at 16:38):

Things get a lot more complicated when you need higher higher constructors like coh : (z : Z) → ap_succ(sec(z)) =ret(succ(z)) there

Alex J. Best (May 11 2021 at 16:42):

The associated talk by Thorsten is quite good iirc https://www.youtube.com/watch?v=Fov95A2bGDI

Mac (May 11 2021 at 18:09):

Yakov Pechersky said:

Now, Mario showed above that one can actually construct an actual type that can be shown to have a my_int instance. But not all postulated collections are valid. So whatever higher inductive type you make, you'd have to show that it doesn't imply False

It is important to note though, that even if your axioms schema does imply False with "synthetic mathematics" approach by Yakov Pechersky i,e,

Yakov Pechersky said:

If you want to do "synthetic mathematics" you can do the following:

class my_int (s : Type) where
  zero : s
  succ : s → s
  pred : s → s
  eq1 : ∀ {a : s}, succ (pred a) = a
  eq2 : ∀ {a : s}, pred (succ a) = a

and

Yakov Pechersky said:

Then you can postulate

variable (s : Type _) [my_int s]

False will only be provable in places s is in scope. You will not have rendered Lean as a whole inconsistent (because you will not actually be able to construct an instance of my_int in a vacuum).

Mario Carneiro (May 11 2021 at 18:12):

That's probably not much consolation if you want to work with my_int though

Mac (May 11 2021 at 21:19):

True, though luckily my_int does not prove False (at least I hope so XD).

Brandon Brown (Jun 20 2021 at 14:48):

So the inductive relation defined by @Mario Carneiro above

inductive int_base.rel : int_base → int_base → Prop
| succ_congr : rel a b → rel (succ a) (succ b)
| pred_congr : rel a b → rel (pred a) (pred b)
| succ_pred : rel (succ (pred a)) a
| pred_succ : rel (pred (succ a)) a

appears not equivalent to the subtype version of the integers I defined elsewhere based on if it's in norm form, i.e. { x : base_int // is_norm (x)}
because I want e.g. a.succ.succ.pred.pred to be equal to zero whereas with this relation that doesn't appear to be true. I've instead defined a relation using the norm function Mario wrote. But was hoping someone could give me some clues on how to make progress on the proof that my addition function on the base integer type respects the relation so I can lift it to the quotient type. I think this new relation can be easily made into an equivalence relation but not sure if using Quotient rather than Quot buys me anything in this particular case.

inductive b_int : Type where
| zero : b_int
| succ : b_int → b_int
| pred : b_int → b_int
deriving DecidableEq

open b_int

def up : b_int → b_int
| (pred a) => a
| a => succ a

def down : b_int → b_int
| (succ a) => a
| a => pred a

def norm_aux : b_int → b_int → b_int :=
  fun a b =>
  match b with
  | zero => a
  | succ b => norm_aux (up a) b
  | pred b => norm_aux (down a) b

def norm : b_int → b_int := norm_aux zero

protected inductive b_int.rel : b_int → b_int → Prop
| refl : (norm a) = (norm b) → b_int.rel a b
| succ_congr : b_int.rel a b → b_int.rel (succ a) (succ b)
| pred_congr : b_int.rel a b → b_int.rel (pred a) (pred b)

def int := Quot b_int.rel

protected def int.succ (a : int) : int := a.lift (fun (a : b_int) => Quot.mk b_int.rel a.succ)
  fun (a b : b_int) (h : b_int.rel a b) => Quot.sound (b_int.rel.succ_congr h)

protected def int.pred (a : int) : int := a.lift (fun (a : b_int) => Quot.mk b_int.rel a.pred)
  fun (a b : b_int) (h : b_int.rel a b) => Quot.sound (b_int.rel.pred_congr h)

instance : Coe b_int int where
  coe (a : b_int) := Quot.mk b_int.rel a

protected def b_int.add (a b : b_int) : int :=
  match a with
  | zero => Quot.mk b_int.rel b
  | succ a => (b_int.add a b).succ
  | pred a => (b_int.add a b).pred

theorem add_zero : b_int.add zero a = (a : int) := rfl

theorem add_succ : b_int.add a c = b_int.add a b → b_int.add (succ a) c = b_int.add (succ a) b := sorry
theorem add_pred : b_int.add a c = b_int.add a b → b_int.add (pred a) c = b_int.add (pred a) b := sorry
-- Not sure if this is the right direction
theorem add_eq2 : ∀ (c b : b_int), (b_int.rel c b) → b_int.add a c = b_int.add a b := by
  intros c b h
  induction a with
  | zero =>
    show (c:int) = (b:int)
    apply Quot.sound
    assumption
  | succ a h2 =>
    apply add_succ
    assumption
  | pred a h3 =>
    apply add_pred
    assumption

-- have to apply lift twice
def int.add : int → int → int :=
  (Quot.lift (λ a : b_int => Quot.lift (b_int.add a) add_eq2) sorry)

Mario Carneiro (Jun 20 2021 at 14:51):

The relation is not itself an equivalence relation, but the equivalence relation generated by that relation makes a.succ.succ.pred.pred = a because a.succ.succ.pred.pred ~ a.succ.pred ~ a where the two relations are in int_base.rel and they are connected by transitivity

Mario Carneiro (Jun 20 2021 at 14:52):

That is, in int := Quot int_base.rel, [[a.succ.succ.pred.pred]] = [[a.succ.pred]] = [[a]] where we use Quot.sound for the individual equalities and Eq.trans to connect them

Kevin Buzzard (Jun 20 2021 at 14:52):

If you import mathlib's data.quot then you will have access to stuff like quot.lift₂, quotient.lift₂, quotient.map₂ and so on, which might make things easier.

Brandon Brown (Jun 20 2021 at 14:55):

Mathlib4 has quot.lift₂ ?

Mario Carneiro (Jun 20 2021 at 14:56):

mathlib 3 does

Mario Carneiro (Jun 20 2021 at 14:56):

there isn't really anything about what you are doing that needs lean 4

Mario Carneiro (Jun 20 2021 at 14:57):

you might as well learn how to do it in lean 3 where there are more theorems available

Kevin Buzzard (Jun 20 2021 at 14:58):

Apologies, I hadn't noticed what stream we're in. Please feel free to port data.quot to mathlib 4 :-)

Brandon Brown (Jun 22 2021 at 04:09):

Thanks, @Mario Carneiro . I get it now, it didn't occur to me that once I have the quotient my non-equivalence relation becomes an equivalence relation given the quotient sound axiom. Indeed, I can prove

example : (Quot.mk b_int.rel zero) = (Quot.mk b_int.rel zero.pred.pred.succ.succ) := by
  have h1 : Quot.mk b_int.rel zero.pred.succ = Quot.mk b_int.rel (succ (succ (pred (pred zero)))) := by {
    apply Quot.sound;
    apply b_int.rel.succ_congr;
    apply b_int.rel.succ_pred;
  };
  rw [←h1];
  apply int_succ_pred;

Moreover, I got around having to use Quot.lift twice by defining my add function to take as the first argument an int and as the second argument a b_int.

protected def b_int.add (a : int) (b : b_int) : int :=
  match b with
  | zero => a
  | succ b => (b_int.add a b).succ
  | pred b => (b_int.add a b).pred

And I proved it respects the equivalence relation to make it into the desired int.add : int → int → int
I am now content and can move beyond my obsession defining the integers in various ways, now having defined the integers the way lean core does, as a subtype using norm and as a quotient type.

Full Code

Brandon Brown (Jun 22 2021 at 04:15):

And yes Lean 3 would be probably easier but I intend to write some tutorials on Lean 4 on my blog

Last updated: Dec 20 2023 at 11:08 UTC