feat(library/nat): add exponentiation for natural numbers #1

cipher1024 · 2017-02-27T21:36:14Z

No description provided.

…forms of de Morgan’s law

…l cases assuming associativity and commutativity

…simplification rules; improve the interfaces by adding type annotations and making some parameters explicit

…other

joehendrix · 2017-02-28T14:53:42Z

library/data/bitvec.lean

+  protected def list_of_nat : ℕ → ℕ → list bool
+  | 0        x := list.nil
+  | (succ n) x := list_of_nat n (x / 2) ++ [to_bool (x % 2 = 1)]
+
  protected def of_nat : Π (n : ℕ), nat → bitvec n


If seems like it'd make sense to define of_nat in terms of list_of_nat, or just prove everything in terms of of_nat. Also why is list_of_nat reducible?

You're right, list_of_nat doesn't actually need to be reducible and we don't need to duplicate the definition of list_of_nat

joehendrix · 2017-02-28T14:55:37Z

library/data/bitvec.lean

+     (assume h : n % 2 = 0, begin rw h, refl end)
+     (assume h : n % 2 = 1, begin rw h, refl end)
+
+end bitvec


Seems confusing to end bitvec, define a theorem in bitvec, then start namespace bitvec.

That's true. I'll fix it.

joehendrix · 2017-02-28T14:56:43Z

library/data/vector.lean

@@ -92,6 +92,10 @@ end accum
 protected lemma eq {n : ℕ} : ∀ (a1 a2 : vector α n), to_list a1 = to_list a2 → a1 = a2
 | ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl

+@[simp] lemma to_list_tag {n : ℕ} {xs : list α} (Pxs : list.length xs = n)


Where is this theorem needed? It should generally happen automatically in semi reducible contexts.

I thought I needed it but I don't.

joehendrix · 2017-02-28T15:02:29Z

library/init/data/list/lemmas.lean

@@ -154,6 +158,24 @@ by induction l; simph
 @[simp] lemma map_reverse (f : α → β) (l : list α) : map f (reverse l) = reverse (map f l) :=
 by induction l; simph

+lemma reverse_core_append' (xs ys zs : list α) :


reverse_core_append' seems like a more useful lemma than reverse_core_append proper. Maybe just have it and combine it with nil_append as needed.

I've also noticed that Leo intentionally didn't prove any lemmas about reverse core directly. Do we need reverse_core_append[']?

I'm going to check where we need it. Why does Leo not prove anything about reverse_core directly?

I can do without reverse_core_append[']. I'll take it out.

I'm not sure why, I'd guess because it's mostly viewed as an internal function just needed to implement reverse.

joehendrix · 2017-02-28T15:07:35Z

library/init/data/nat/lemmas.lean

+  end
+end
+
+lemma add_le_add_left_iff (n m k : ℕ) : n ≤ m ↔ k + n ≤ k + m


Should the left and right hand sides be reversed for simplification.

joehendrix · 2017-02-28T15:08:48Z

library/init/data/nat/lemmas.lean

+  | (succ n) := by refl
+
+theorem div_le_div
+: ∀ {y x}, x ≤ y → ∀ z : ℕ, x / z ≤ y / z :=


If we added a constraint that z \ne 0, then this could also be used as a simplification lemma if reoriented.

Can you elaborate please? Why can't we use it for simplification as it stands?

I was thinking it might be useful to rewrite x /z <= y / z to x <= y. If Lean's elaborate will already do that, then great. I also don't think that change is critical.

I think I see what you mean. You're suggesting I strengthen the theorem to an equivalence (with z \ne 0 as a side condition). I'll try adding

theorem div_le_div_of_le
: ∀ z : ℕ, z ≠ 0 → x / z ≤ y / z → x ≤ y

and

theorem div_le_div_iff_le
: ∀ z : ℕ, z ≠ 0 → ( x / z ≤ y / z ↔ x ≤ y )

and get back to you.

Actually, I don't think that stronger theorem holds: consider x = 3, y = 2 and z = 2.

x / z = 1
y / z = 1
but 3 ≤ 2 does not hold.

I could prove a Galois connection between / and * though:

x / z ≤ y ↔ x ≤ y * z

Together with indirect equality (see below) it could provide a basis for simpler proofs about division.
theorem indirect_equality [weak_order α] (x y : α) : x = y ↔ (∀ z : α, x ≤ z ↔ y ≤ z)

Should I go ahead?

Good catch; I'm not sure if the generalization matters.

joehendrix · 2017-02-28T15:14:06Z

library/data/bitvec.lean

+open subtype
+
+theorem bitvec.bits_to_nat_over_append (xs : list bool) (y : bool)
+:  bitvec.bits_to_nat (xs ++ [y]) = bitvec.bits_to_nat xs * 2 + bitvec.bits_to_nat [y]  :=


Use consistent indention in this file for proofs.

joehendrix · 2017-02-28T15:18:25Z

library/init/data/list/lemmas.lean

+
+end foldr
+
+section foldr_ac


Were the AC versions of these proofs actually used somewhere? It seems like versions that only depend on associativity would be more generally useful.

I don't think I can remove commutativity from the assumptions of any of those rules. Do you have something in mind about reformulating them without commutativity?

I was thinking associativity + identity would get similar versions, but AC has different variants. These are fine, but I still don't quite see what theorems were important for our proofs. e.g., I see sum_le is important, but doesn't appear to use this work. Conversely, the sum_foldr utility seems less clear.

I could remove sum_foldr and sum_foldl. I put a bit more than we strictly need just so that it doesn't come out uneven. For instance, I tried to prove the same things about foldl and foldr. It allowed me to play around with the proofs and choose the one I prefer. I thought the unused theorems would still be worth keeping.

… commits

joehendrix · 2017-03-01T15:00:56Z

library/init/data/nat/lemmas.lean

+      begin
+        rw [div_def x z,dif_pos Hx,div_def y z,dif_pos Hy,-add_le_add_right_iff] ,
+        apply IH (y - z) Hyz_z Hxy_z
+      end


Could we get these lemmas to match the style of the other proofs in Lean's standard library.

joehendrix · 2017-03-02T07:50:39Z

library/init/data/nat/lemmas.lean

+  | (succ n) := by refl
+
+theorem div_le_div
+: ∀ {y x}, x ≤ y → ∀ z : ℕ, x / z ≤ y / z :=


Good catch; I'm not sure if the generalization matters.

joehendrix · 2017-03-02T07:51:15Z

library/init/data/nat/lemmas.lean

+...    = 1 + z - 1       : by rw -nat.add_sub_assoc Pz
+...    = z               : by rw nat.add_sub_cancel_left,
+    have Pdiv : 0 < z ∧ z ≤ z * x + z - 1, from ⟨Pz,Pz_le_zx_z_1⟩,
+    calc


I'd recommend a final pass to see if these proofs can be simplified via the tactics language.

Simon Hudon added 8 commits February 27, 2017 13:30

feat(library/nat): add exponentiation for natural numbers

4483159

feat(library/logic): add various forms, classical and non-classical, …

8048045

…forms of de Morgan’s law

feat(library/nat): add useful rules to reason about division and modulo

6b3893a

feat(library/init/list): add theorems about foldl / foldr with specia…

103f688

…l cases assuming associativity and commutativity

style(library/list,library/nat): simplify proofs by adding automatic …

43699d5

…simplification rules; improve the interfaces by adding type annotations and making some parameters explicit

feat(library/bitvec): add a proof that to_nat and of_nat cancel each …

5014a7d

…other

feat(library/list): add rules for reasoning about sums

0b07bcf

feat(library/list): add a rule to simplify the sum of singleton lists

a4cbd25

joehendrix reviewed Feb 28, 2017

View reviewed changes

fix(library/bitvec,vector,list): addressed Joe’s comments on previous…

839828c

… commits

joehendrix reviewed Mar 1, 2017

View reviewed changes

joehendrix reviewed Mar 2, 2017

View reviewed changes

joehendrix merged commit ac638f2 into GaloisInc:master Mar 2, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(library/nat): add exponentiation for natural numbers #1

feat(library/nat): add exponentiation for natural numbers #1

cipher1024 commented Feb 27, 2017

joehendrix Feb 28, 2017

cipher1024 Feb 28, 2017

joehendrix Feb 28, 2017

cipher1024 Feb 28, 2017

joehendrix Feb 28, 2017

cipher1024 Feb 28, 2017

joehendrix Feb 28, 2017

joehendrix Feb 28, 2017

cipher1024 Feb 28, 2017

joehendrix Mar 1, 2017

joehendrix Feb 28, 2017

cipher1024 Mar 1, 2017

joehendrix Feb 28, 2017

cipher1024 Mar 1, 2017

joehendrix Mar 1, 2017

cipher1024 Mar 1, 2017

cipher1024 Mar 1, 2017

joehendrix Mar 2, 2017

joehendrix Feb 28, 2017

cipher1024 Feb 28, 2017

joehendrix Feb 28, 2017

cipher1024 Mar 1, 2017

joehendrix Mar 1, 2017

cipher1024 Mar 1, 2017

joehendrix Mar 1, 2017

joehendrix Mar 2, 2017

joehendrix Mar 2, 2017

feat(library/nat): add exponentiation for natural numbers #1

feat(library/nat): add exponentiation for natural numbers #1

Conversation

cipher1024 commented Feb 27, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment