From fc7da8d9b1e0456b433e3990c3810cdad3556d85 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 15 Aug 2021 21:24:20 +0000 Subject: [PATCH] chore(data/vector3): extract to a new file (#8669) This is simply a file move, with no other changes other than a minimal docstring. In it's old location this was very hard to find. --- src/data/vector3.lean | 188 +++++++++++++++++++++++++++++++++++ src/number_theory/dioph.lean | 168 +------------------------------ 2 files changed, 189 insertions(+), 167 deletions(-) create mode 100644 src/data/vector3.lean diff --git a/src/data/vector3.lean b/src/data/vector3.lean new file mode 100644 index 0000000000000..667a149fd2cbe --- /dev/null +++ b/src/data/vector3.lean @@ -0,0 +1,188 @@ +/- +Copyright (c) 2017 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ +import data.fin2 +import tactic.localized + +/-! +# Alternate definition of `vector` in terms of `fin2` + +This file provides a locale `vector3` which overrides `[a, b, c]` notation to create `vector3` not +`list`. + +The `::` notation is overloaded by this file to mean `vector3.cons`. +-/ + +universes u + +open fin2 nat + +/-- Alternate definition of `vector` based on `fin2`. -/ +def vector3 (α : Type u) (n : ℕ) : Type u := fin2 n → α + +namespace vector3 + +/-- The empty vector -/ +@[pattern] def nil {α} : vector3 α 0. + +/-- The vector cons operation -/ +@[pattern] def cons {α} {n} (a : α) (v : vector3 α n) : vector3 α (succ n) := +λi, by {refine i.cases' _ _, exact a, exact v} + +/- We do not want to make the following notation global, because then these expressions will be +overloaded, and only the expected type will be able to disambiguate the meaning. Worse: Lean will +try to insert a coercion from `vector3 α _` to `list α`, if a list is expected. -/ +localized "notation `[` l:(foldr `, ` (h t, vector3.cons h t) nil `]`) := l" in vector3 +notation a :: b := cons a b + +@[simp] theorem cons_fz {α} {n} (a : α) (v : vector3 α n) : (a :: v) fz = a := rfl +@[simp] theorem cons_fs {α} {n} (a : α) (v : vector3 α n) (i) : (a :: v) (fs i) = v i := rfl + +/-- Get the `i`th element of a vector -/ +@[reducible] def nth {α} {n} (i : fin2 n) (v : vector3 α n) : α := v i + +/-- Construct a vector from a function on `fin2`. -/ +@[reducible] def of_fn {α} {n} (f : fin2 n → α) : vector3 α n := f + +/-- Get the head of a nonempty vector. -/ +def head {α} {n} (v : vector3 α (succ n)) : α := v fz + +/-- Get the tail of a nonempty vector. -/ +def tail {α} {n} (v : vector3 α (succ n)) : vector3 α n := λi, v (fs i) + +theorem eq_nil {α} (v : vector3 α 0) : v = [] := +funext $ λi, match i with end + +theorem cons_head_tail {α} {n} (v : vector3 α (succ n)) : head v :: tail v = v := +funext $ λi, fin2.cases' rfl (λ_, rfl) i + +def nil_elim {α} {C : vector3 α 0 → Sort u} (H : C []) (v : vector3 α 0) : C v := +by rw eq_nil v; apply H + +def cons_elim {α n} {C : vector3 α (succ n) → Sort u} (H : Π (a : α) (t : vector3 α n), C (a :: t)) + (v : vector3 α (succ n)) : C v := +by rw ← (cons_head_tail v); apply H + +@[simp] theorem cons_elim_cons {α n C H a t} : @cons_elim α n C H (a :: t) = H a t := rfl + +@[elab_as_eliminator] +protected def rec_on {α} {C : Π {n}, vector3 α n → Sort u} {n} (v : vector3 α n) + (H0 : C []) + (Hs : Π {n} (a) (w : vector3 α n), C w → C (a :: w)) : C v := +nat.rec_on n + (λv, v.nil_elim H0) + (λn IH v, v.cons_elim (λa t, Hs _ _ (IH _))) v + +@[simp] theorem rec_on_nil {α C H0 Hs} : @vector3.rec_on α @C 0 [] H0 @Hs = H0 := +rfl + +@[simp] theorem rec_on_cons {α C H0 Hs n a v} : + @vector3.rec_on α @C (succ n) (a :: v) H0 @Hs = Hs a v (@vector3.rec_on α @C n v H0 @Hs) := +rfl + +/-- Append two vectors -/ +def append {α} {m} (v : vector3 α m) {n} (w : vector3 α n) : vector3 α (n+m) := +nat.rec_on m (λ_, w) (λm IH v, v.cons_elim $ λa t, @fin2.cases' (n+m) (λ_, α) a (IH t)) v + +local infix ` +-+ `:65 := vector3.append + +@[simp] theorem append_nil {α} {n} (w : vector3 α n) : [] +-+ w = w := rfl + +@[simp] theorem append_cons {α} (a : α) {m} (v : vector3 α m) {n} (w : vector3 α n) : + (a::v) +-+ w = a :: (v +-+ w) := rfl + +@[simp] theorem append_left {α} : ∀ {m} (i : fin2 m) (v : vector3 α m) {n} (w : vector3 α n), + (v +-+ w) (left n i) = v i +| ._ (@fz m) v n w := v.cons_elim (λa t, by simp [*, left]) +| ._ (@fs m i) v n w := v.cons_elim (λa t, by simp [*, left]) + +@[simp] theorem append_add {α} : ∀ {m} (v : vector3 α m) {n} (w : vector3 α n) (i : fin2 n), + (v +-+ w) (add i m) = w i +| 0 v n w i := rfl +| (succ m) v n w i := v.cons_elim (λa t, by simp [*, add]) + +/-- Insert `a` into `v` at index `i`. -/ +def insert {α} (a : α) {n} (v : vector3 α n) (i : fin2 (succ n)) : vector3 α (succ n) := +λj, (a :: v) (insert_perm i j) + +@[simp] theorem insert_fz {α} (a : α) {n} (v : vector3 α n) : insert a v fz = a :: v := +by refine funext (λj, j.cases' _ _); intros; refl + +@[simp] theorem insert_fs {α} (a : α) {n} (b : α) (v : vector3 α n) (i : fin2 (succ n)) : + insert a (b :: v) (fs i) = b :: insert a v i := +funext $ λj, by { + refine j.cases' _ (λj, _); simp [insert, insert_perm], + refine fin2.cases' _ _ (insert_perm i j); simp [insert_perm] } + +theorem append_insert {α} (a : α) {k} (t : vector3 α k) {n} (v : vector3 α n) (i : fin2 (succ n)) + (e : succ n + k = succ (n + k)) : + insert a (t +-+ v) (eq.rec_on e (i.add k)) = eq.rec_on e (t +-+ insert a v i) := +begin + refine vector3.rec_on t (λe, _) (λk b t IH e, _) e, refl, + have e' := succ_add n k, + change insert a (b :: (t +-+ v)) (eq.rec_on (congr_arg succ e') (fs (add i k))) + = eq.rec_on (congr_arg succ e') (b :: (t +-+ insert a v i)), + rw ← (eq.drec_on e' rfl : fs (eq.rec_on e' (i.add k) : fin2 (succ (n + k))) = eq.rec_on + (congr_arg succ e') (fs (i.add k))), + simp, rw IH, exact eq.drec_on e' rfl +end + +end vector3 + +section vector3 +open vector3 +open_locale vector3 + +/-- "Curried" exists, i.e. ∃ x1 ... xn, f [x1, ..., xn] -/ +def vector_ex {α} : Π k, (vector3 α k → Prop) → Prop +| 0 f := f [] +| (succ k) f := ∃x : α, vector_ex k (λv, f (x :: v)) + +/-- "Curried" forall, i.e. ∀ x1 ... xn, f [x1, ..., xn] -/ +def vector_all {α} : Π k, (vector3 α k → Prop) → Prop +| 0 f := f [] +| (succ k) f := ∀x : α, vector_all k (λv, f (x :: v)) + +theorem exists_vector_zero {α} (f : vector3 α 0 → Prop) : Exists f ↔ f [] := +⟨λ⟨v, fv⟩, by rw ← (eq_nil v); exact fv, λf0, ⟨[], f0⟩⟩ + +theorem exists_vector_succ {α n} (f : vector3 α (succ n) → Prop) : Exists f ↔ ∃x v, f (x :: v) := +⟨λ⟨v, fv⟩, ⟨_, _, by rw cons_head_tail v; exact fv⟩, λ⟨x, v, fxv⟩, ⟨_, fxv⟩⟩ + +theorem vector_ex_iff_exists {α} : ∀ {n} (f : vector3 α n → Prop), vector_ex n f ↔ Exists f +| 0 f := (exists_vector_zero f).symm +| (succ n) f := iff.trans (exists_congr (λx, vector_ex_iff_exists _)) (exists_vector_succ f).symm + +theorem vector_all_iff_forall {α} : ∀ {n} (f : vector3 α n → Prop), vector_all n f ↔ ∀ v, f v +| 0 f := ⟨λf0 v, v.nil_elim f0, λal, al []⟩ +| (succ n) f := (forall_congr (λx, vector_all_iff_forall (λv, f (x :: v)))).trans + ⟨λal v, v.cons_elim al, λal x v, al (x::v)⟩ + +/-- `vector_allp p v` is equivalent to `∀ i, p (v i)`, but unfolds directly to a conjunction, + i.e. `vector_allp p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/ +def vector_allp {α} (p : α → Prop) {n} (v : vector3 α n) : Prop := +vector3.rec_on v true (λn a v IH, @vector3.rec_on _ (λn v, Prop) _ v (p a) (λn b v' _, p a ∧ IH)) + +@[simp] theorem vector_allp_nil {α} (p : α → Prop) : vector_allp p [] = true := rfl +@[simp] theorem vector_allp_singleton {α} (p : α → Prop) (x : α) : vector_allp p [x] = p x := rfl +@[simp] theorem vector_allp_cons {α} (p : α → Prop) {n} (x : α) (v : vector3 α n) : + vector_allp p (x :: v) ↔ p x ∧ vector_allp p v := +vector3.rec_on v (and_true _).symm (λn a v IH, iff.rfl) + +theorem vector_allp_iff_forall {α} (p : α → Prop) {n} (v : vector3 α n) : + vector_allp p v ↔ ∀ i, p (v i) := +begin refine v.rec_on _ _, + { exact ⟨λ_, fin2.elim0, λ_, trivial⟩ }, + { simp, refine λn a v IH, (and_congr_right (λ_, IH)).trans + ⟨λ⟨pa, h⟩ i, by {refine i.cases' _ _, exacts [pa, h]}, λh, ⟨_, λi, _⟩⟩, + { have h0 := h fz, simp at h0, exact h0 }, + { have hs := h (fs i), simp at hs, exact hs } } +end + +theorem vector_allp.imp {α} {p q : α → Prop} (h : ∀ x, p x → q x) + {n} {v : vector3 α n} (al : vector_allp p v) : vector_allp q v := +(vector_allp_iff_forall _ _).2 (λi, h _ $ (vector_allp_iff_forall _ _).1 al _) + +end vector3 diff --git a/src/number_theory/dioph.lean b/src/number_theory/dioph.lean index f57f5301c43cb..821d7771976e1 100644 --- a/src/number_theory/dioph.lean +++ b/src/number_theory/dioph.lean @@ -7,6 +7,7 @@ Authors: Mario Carneiro import number_theory.pell import data.pfun import data.fin2 +import data.vector3 /-! # Diophantine functions and Matiyasevic's theorem @@ -65,173 +66,6 @@ end int open fin2 -/-- Alternate definition of `vector` based on `fin2`. -/ -def vector3 (α : Type u) (n : ℕ) : Type u := fin2 n → α - -namespace vector3 - -/-- The empty vector -/ -@[pattern] def nil {α} : vector3 α 0. - -/-- The vector cons operation -/ -@[pattern] def cons {α} {n} (a : α) (v : vector3 α n) : vector3 α (succ n) := -λi, by {refine i.cases' _ _, exact a, exact v} - -/- We do not want to make the following notation global, because then these expressions will be -overloaded, and only the expected type will be able to disambiguate the meaning. Worse: Lean will -try to insert a coercion from `vector3 α _` to `list α`, if a list is expected. -/ -localized "notation `[` l:(foldr `, ` (h t, vector3.cons h t) nil `]`) := l" in vector3 -notation a :: b := cons a b - -@[simp] theorem cons_fz {α} {n} (a : α) (v : vector3 α n) : (a :: v) fz = a := rfl -@[simp] theorem cons_fs {α} {n} (a : α) (v : vector3 α n) (i) : (a :: v) (fs i) = v i := rfl - -/-- Get the `i`th element of a vector -/ -@[reducible] def nth {α} {n} (i : fin2 n) (v : vector3 α n) : α := v i - -/-- Construct a vector from a function on `fin2`. -/ -@[reducible] def of_fn {α} {n} (f : fin2 n → α) : vector3 α n := f - -/-- Get the head of a nonempty vector. -/ -def head {α} {n} (v : vector3 α (succ n)) : α := v fz - -/-- Get the tail of a nonempty vector. -/ -def tail {α} {n} (v : vector3 α (succ n)) : vector3 α n := λi, v (fs i) - -theorem eq_nil {α} (v : vector3 α 0) : v = [] := -funext $ λi, match i with end - -theorem cons_head_tail {α} {n} (v : vector3 α (succ n)) : head v :: tail v = v := -funext $ λi, fin2.cases' rfl (λ_, rfl) i - -def nil_elim {α} {C : vector3 α 0 → Sort u} (H : C []) (v : vector3 α 0) : C v := -by rw eq_nil v; apply H - -def cons_elim {α n} {C : vector3 α (succ n) → Sort u} (H : Π (a : α) (t : vector3 α n), C (a :: t)) - (v : vector3 α (succ n)) : C v := -by rw ← (cons_head_tail v); apply H - -@[simp] theorem cons_elim_cons {α n C H a t} : @cons_elim α n C H (a :: t) = H a t := rfl - -@[elab_as_eliminator] -protected def rec_on {α} {C : Π {n}, vector3 α n → Sort u} {n} (v : vector3 α n) - (H0 : C []) - (Hs : Π {n} (a) (w : vector3 α n), C w → C (a :: w)) : C v := -nat.rec_on n - (λv, v.nil_elim H0) - (λn IH v, v.cons_elim (λa t, Hs _ _ (IH _))) v - -@[simp] theorem rec_on_nil {α C H0 Hs} : @vector3.rec_on α @C 0 [] H0 @Hs = H0 := -rfl - -@[simp] theorem rec_on_cons {α C H0 Hs n a v} : - @vector3.rec_on α @C (succ n) (a :: v) H0 @Hs = Hs a v (@vector3.rec_on α @C n v H0 @Hs) := -rfl - -/-- Append two vectors -/ -def append {α} {m} (v : vector3 α m) {n} (w : vector3 α n) : vector3 α (n+m) := -nat.rec_on m (λ_, w) (λm IH v, v.cons_elim $ λa t, @fin2.cases' (n+m) (λ_, α) a (IH t)) v - -local infix ` +-+ `:65 := vector3.append - -@[simp] theorem append_nil {α} {n} (w : vector3 α n) : [] +-+ w = w := rfl - -@[simp] theorem append_cons {α} (a : α) {m} (v : vector3 α m) {n} (w : vector3 α n) : - (a::v) +-+ w = a :: (v +-+ w) := rfl - -@[simp] theorem append_left {α} : ∀ {m} (i : fin2 m) (v : vector3 α m) {n} (w : vector3 α n), - (v +-+ w) (left n i) = v i -| ._ (@fz m) v n w := v.cons_elim (λa t, by simp [*, left]) -| ._ (@fs m i) v n w := v.cons_elim (λa t, by simp [*, left]) - -@[simp] theorem append_add {α} : ∀ {m} (v : vector3 α m) {n} (w : vector3 α n) (i : fin2 n), - (v +-+ w) (add i m) = w i -| 0 v n w i := rfl -| (succ m) v n w i := v.cons_elim (λa t, by simp [*, add]) - -/-- Insert `a` into `v` at index `i`. -/ -def insert {α} (a : α) {n} (v : vector3 α n) (i : fin2 (succ n)) : vector3 α (succ n) := -λj, (a :: v) (insert_perm i j) - -@[simp] theorem insert_fz {α} (a : α) {n} (v : vector3 α n) : insert a v fz = a :: v := -by refine funext (λj, j.cases' _ _); intros; refl - -@[simp] theorem insert_fs {α} (a : α) {n} (b : α) (v : vector3 α n) (i : fin2 (succ n)) : - insert a (b :: v) (fs i) = b :: insert a v i := -funext $ λj, by { - refine j.cases' _ (λj, _); simp [insert, insert_perm], - refine fin2.cases' _ _ (insert_perm i j); simp [insert_perm] } - -theorem append_insert {α} (a : α) {k} (t : vector3 α k) {n} (v : vector3 α n) (i : fin2 (succ n)) - (e : succ n + k = succ (n + k)) : - insert a (t +-+ v) (eq.rec_on e (i.add k)) = eq.rec_on e (t +-+ insert a v i) := -begin - refine vector3.rec_on t (λe, _) (λk b t IH e, _) e, refl, - have e' := succ_add n k, - change insert a (b :: (t +-+ v)) (eq.rec_on (congr_arg succ e') (fs (add i k))) - = eq.rec_on (congr_arg succ e') (b :: (t +-+ insert a v i)), - rw ← (eq.drec_on e' rfl : fs (eq.rec_on e' (i.add k) : fin2 (succ (n + k))) = eq.rec_on - (congr_arg succ e') (fs (i.add k))), - simp, rw IH, exact eq.drec_on e' rfl -end - -end vector3 - -section vector3 -open vector3 -open_locale vector3 - -/-- "Curried" exists, i.e. ∃ x1 ... xn, f [x1, ..., xn] -/ -def vector_ex {α} : Π k, (vector3 α k → Prop) → Prop -| 0 f := f [] -| (succ k) f := ∃x : α, vector_ex k (λv, f (x :: v)) - -/-- "Curried" forall, i.e. ∀ x1 ... xn, f [x1, ..., xn] -/ -def vector_all {α} : Π k, (vector3 α k → Prop) → Prop -| 0 f := f [] -| (succ k) f := ∀x : α, vector_all k (λv, f (x :: v)) - -theorem exists_vector_zero {α} (f : vector3 α 0 → Prop) : Exists f ↔ f [] := -⟨λ⟨v, fv⟩, by rw ← (eq_nil v); exact fv, λf0, ⟨[], f0⟩⟩ - -theorem exists_vector_succ {α n} (f : vector3 α (succ n) → Prop) : Exists f ↔ ∃x v, f (x :: v) := -⟨λ⟨v, fv⟩, ⟨_, _, by rw cons_head_tail v; exact fv⟩, λ⟨x, v, fxv⟩, ⟨_, fxv⟩⟩ - -theorem vector_ex_iff_exists {α} : ∀ {n} (f : vector3 α n → Prop), vector_ex n f ↔ Exists f -| 0 f := (exists_vector_zero f).symm -| (succ n) f := iff.trans (exists_congr (λx, vector_ex_iff_exists _)) (exists_vector_succ f).symm - -theorem vector_all_iff_forall {α} : ∀ {n} (f : vector3 α n → Prop), vector_all n f ↔ ∀ v, f v -| 0 f := ⟨λf0 v, v.nil_elim f0, λal, al []⟩ -| (succ n) f := (forall_congr (λx, vector_all_iff_forall (λv, f (x :: v)))).trans - ⟨λal v, v.cons_elim al, λal x v, al (x::v)⟩ - -/-- `vector_allp p v` is equivalent to `∀ i, p (v i)`, but unfolds directly to a conjunction, - i.e. `vector_allp p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/ -def vector_allp {α} (p : α → Prop) {n} (v : vector3 α n) : Prop := -vector3.rec_on v true (λn a v IH, @vector3.rec_on _ (λn v, Prop) _ v (p a) (λn b v' _, p a ∧ IH)) - -@[simp] theorem vector_allp_nil {α} (p : α → Prop) : vector_allp p [] = true := rfl -@[simp] theorem vector_allp_singleton {α} (p : α → Prop) (x : α) : vector_allp p [x] = p x := rfl -@[simp] theorem vector_allp_cons {α} (p : α → Prop) {n} (x : α) (v : vector3 α n) : - vector_allp p (x :: v) ↔ p x ∧ vector_allp p v := -vector3.rec_on v (and_true _).symm (λn a v IH, iff.rfl) - -theorem vector_allp_iff_forall {α} (p : α → Prop) {n} (v : vector3 α n) : - vector_allp p v ↔ ∀ i, p (v i) := -begin refine v.rec_on _ _, - { exact ⟨λ_, fin2.elim0, λ_, trivial⟩ }, - { simp, refine λn a v IH, (and_congr_right (λ_, IH)).trans - ⟨λ⟨pa, h⟩ i, by {refine i.cases' _ _, exacts [pa, h]}, λh, ⟨_, λi, _⟩⟩, - { have h0 := h fz, simp at h0, exact h0 }, - { have hs := h (fs i), simp at hs, exact hs } } -end - -theorem vector_allp.imp {α} {p q : α → Prop} (h : ∀ x, p x → q x) - {n} {v : vector3 α n} (al : vector_allp p v) : vector_allp q v := -(vector_allp_iff_forall _ _).2 (λi, h _ $ (vector_allp_iff_forall _ _).1 al _) -end vector3 - /-- `list_all p l` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e. `list_all p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/ @[simp] def list_all {α} (p : α → Prop) : list α → Prop