variable {F : Type} theorem succ_not_zero (n : Nat) (h : Na...

Prompt

variable {F : Type} theorem succ_not_zero (n : Nat) (h : Nat.succ n = 0) : False := nomatch h theorem zero_not_succ (n : Nat) (h : 0 = Nat.succ n) : False := nomatch h theorem succ_inj {n m : Nat} (h : Nat.succ n = Nat.succ m) : n = m := congrArg (fun x => match x with | 0 => 0 | Nat.succ k => k) h theorem nat_zero_add : (m : Nat) → 0 + m = m | 0 => Eq.refl 0 | Nat.succ m => congrArg Nat.succ (nat_zero_add m) theorem nat_succ_add (n : Nat) : (m : Nat) → Nat.succ n + m = Nat.succ (n + m) | 0 => Eq.refl (Nat.succ n) | Nat.succ m => congrArg Nat.succ (nat_succ_add n m) theorem congr_cons {α : Type} {x y : α} {xs ys : List α} (hx : x = y) (hxs : xs = ys) : x :: xs = y :: ys := match hx, hxs with | Eq.refl _, Eq.refl _ => Eq.refl _ theorem congr_append {α : Type} {xs ys us vs : List α} (h1 : xs = ys) (h2 : us = vs) : xs ++ us = ys ++ vs := match h1, h2 with | Eq.refl _, Eq.refl _ => Eq.refl _ theorem congr_add {n1 n2 m1 m2 : Nat} (h1 : n1 = n2) (h2 : m1 = m2) : n1 + m1 = n2 + m2 := match h1, h2 with | Eq.refl _, Eq.refl _ => Eq.refl _ theorem congr_pair {α β : Type} {a b : α} {c d : β} (h1 : a = b) (h2 : c = d) : (a, c) = (b, d) := match h1, h2 with | Eq.refl _, Eq.refl _ => Eq.refl _ def split_at (n : Nat) (L : List F) : List F × List F := match n with | 0 => ([], L) | Nat.succ k => match L with | [] => ([], []) | x :: xs => let (l1, l2) := split_at k xs (x :: l1, l2) theorem split_at_lengths_gen : (n m : Nat) → (L : List F) → L.length = n + m → (split_at n L).1.length = n ∧ (split_at n L).2.length = m | 0, m, _L, h => let _ := _L ⟨Eq.refl 0, Eq.trans h (nat_zero_add m)⟩ | Nat.succ n, m, [], h => False.elim (zero_not_succ (n + m) (Eq.trans h (nat_succ_add n m))) | Nat.succ n, m, _ :: xs, h => let h' : Nat.succ xs.length = Nat.succ (n + m) := Eq.trans h (nat_succ_add n m) let h_len : xs.length = n + m := succ_inj h' let rec_res := split_at_lengths_gen n m xs h_len ⟨congrArg Nat.succ rec_res.left, rec_res.right⟩ theorem split_at_reconstruct : (n : Nat) → (L : List F) → (split_at n L).1 ++ (split_at n L).2 = L | 0, L => Eq.refl L | Nat.succ _, [] => Eq.refl [] | Nat.succ n, x :: xs => congrArg (List.cons x) (split_at_reconstruct n xs) theorem split_at_append : (n : Nat) → (L1 L2 : List F) → L1.length = n → split_at n (L1 ++ L2) = (L1, L2) | 0, [], L2, _ => Eq.refl ([], L2) | 0, _ :: _, _, h => False.elim (succ_not_zero _ h) | Nat.succ n, x :: xs, L2, h => congrArg (fun p => (x :: p.1, p.2)) (split_at_append n xs L2 (succ_inj h)) | Nat.succ _, [], _, h => False.elim (zero_not_succ _ h) theorem length_zipWith : (f : F → F → F) → (L1 L2 : List F) → L1.length = L2.length → (List.zipWith f L1 L2).length = L1.length | _, [], [], _ => Eq.refl 0 | f, _ :: xs, _ :: ys, h => congrArg Nat.succ (length_zipWith f xs ys (succ_inj h)) | _, _ :: _, [], h => False.elim (succ_not_zero _ h) | _, [], _ :: _, h => False.elim (zero_not_succ _ h) theorem length_append : (L1 L2 : List F) → (L1 ++ L2).length = L1.length + L2.length | [], L2 => Eq.symm (nat_zero_add L2.length) | _ :: xs, L2 => Eq.trans (congrArg Nat.succ (length_append xs L2)) (Eq.symm (nat_succ_add xs.length L2.length)) theorem zipWith_zipWith (f1 f2 g : F → F → F) : (L1 L2 : List F) → L1.length = L2.length → List.zipWith g (List.zipWith f1 L1 L2) (List.zipWith f2 L1 L2) = List.zipWith (fun a b => g (f1 a b) (f2 a b)) L1 L2 | [], [], _ => Eq.refl [] | x :: xs, y :: ys, h => congr_cons (Eq.refl (g (f1 x y) (f2 x y))) (zipWith_zipWith f1 f2 g xs ys (succ_inj h)) | _ :: _, [], h => False.elim (succ_not_zero _ h) | [], _ :: _, h => False.elim (zero_not_succ _ h) theorem zipWith_congr {f g : F → F → F} (h : ∀ a b : F, f a b = g a b) : (L1 L2 : List F) → List.zipWith f L1 L2 = List.zipWith g L1 L2 | [], _ => Eq.refl [] | _ :: _, [] => Eq.refl [] | x :: xs, y :: ys => congr_cons (h x y) (zipWith_congr h xs ys) theorem zipWith_fst : (L1 L2 : List F) → L1.length = L2.length → List.zipWith (fun a _ => a) L1 L2 = L1 | [], [], _ => Eq.refl [] | x :: xs, _ :: ys, h => congr_cons (Eq.refl x) (zipWith_fst xs ys (succ_inj h)) | _ :: _, [], h => False.elim (succ_not_zero _ h) | [], _ :: _, h => False.elim (zero_not_succ _ h) theorem zipWith_snd : (L1 L2 : List F) → L1.length = L2.length → List.zipWith (fun _ b => b) L1 L2 = L2 | [], [], _ => Eq.refl [] | _ :: xs, y :: ys, h => congr_cons (Eq.refl y) (zipWith_snd xs ys (succ_inj h)) | _ :: _, [], h => False.elim (succ_not_zero _ h) | [], _ :: _, h => False.elim (zero_not_succ _ h) theorem zipWith_fst_snd_reconstruct (dim : Nat) (L : List F) (h : L.length = dim + dim) : List.zipWith (fun a _ => a) (split_at dim L).1 (split_at dim L).2 ++ List.zipWith (fun _ b => b) (split_at dim L).1 (split_at dim L).2 = L := Eq.trans (congr_append (zipWith_fst (split_at dim L).1 (split_at dim L).2 (Eq.trans (split_at_lengths_gen dim dim L h).left (Eq.symm (split_at_lengths_gen dim dim L h).right))) (zipWith_snd (split_at dim L).1 (split_at dim L).2 (Eq.trans (split_at_lengths_gen dim dim L h).left (Eq.symm (split_at_lengths_gen dim dim L h).right)))) (split_at_reconstruct dim L) def repeat_value : Nat → F → List F | 0, _ => [] | Nat.succ n, a => a :: repeat_value n a theorem length_repeat_value : (n : Nat) → (a : F) → (repeat_value n a).length = n | 0, _ => Eq.refl 0 | Nat.succ n, a => congrArg Nat.succ (length_repeat_value n a) theorem zipWith_repeat_value (f : F → F → F) (n : Nat) (a b : F) : List.zipWith f (repeat_value n a) (repeat_value n b) = repeat_value n (f a b) | 0 => Eq.refl [] | Nat.succ n => congr_cons (Eq.refl (f a b)) (zipWith_repeat_value f n a b) def pairData (dim : Nat) (p : F × F) : List F := repeat_value dim p.1 ++ repeat_value dim p.2 theorem length_pairData (dim : Nat) (p : F × F) : (pairData dim p).length = dim + dim := Eq.trans (length_append (repeat_value dim p.1) (repeat_value dim p.2)) (congr_add (length_repeat_value dim p.1) (length_repeat_value dim p.2)) theorem split_at_pairData (dim : Nat) (p : F × F) : split_at dim (pairData dim p) = (repeat_value dim p.1, repeat_value dim p.2) := split_at_append dim (repeat_value dim p.1) (repeat_value dim p.2) (length_repeat_value dim p.1) structure ScaleAlgebra (F : Type) where add : F → F → F sub : F → F → F mul : F → F → F scale : F exists_distinct : ∃ a b : F, a ≠ b def forwardCore (sa : ScaleAlgebra F) (dim : Nat) (L : List F) : List F := let g1 := (split_at dim L).1 let g2 := (split_at dim L).2 let h1_new := List.zipWith (fun a b => sa.mul (sa.add a b) sa.scale) g1 g2 let h2_new := List.zipWith (fun a b => sa.mul (sa.sub b a) sa.scale) g1 g2 h1_new ++ h2_new theorem forwardCore_pairData (sa : ScaleAlgebra F) (dim : Nat) (p : F × F) : forwardCore sa dim (pairData dim p) = pairData dim (sa.mul (sa.add p.1 p.2) sa.scale, sa.mul (sa.sub p.2 p.1) sa.scale) := congr_append (Eq.trans (congrArg (fun parts : List F × List F => List.zipWith (fun a b => sa.mul (sa.add a b) sa.scale) parts.1 parts.2) (split_at_pairData dim p)) (zipWith_repeat_value (fun a b => sa.mul (sa.add a b) sa.scale) dim p.1 p.2)) (Eq.trans (congrArg (fun parts : List F × List F => List.zipWith (fun a b => sa.mul (sa.sub b a) sa.scale) parts.1 parts.2) (split_at_pairData dim p)) (zipWith_repeat_value (fun a b => sa.mul (sa.sub b a) sa.scale) dim p.1 p.2)) theorem length_forwardCore (sa : ScaleAlgebra F) (dim : Nat) (L : List F) (h : L.length = dim + dim) : (forwardCore sa dim L).length = dim + dim := let g1 := (split_at dim L).1 let g2 := (split_at dim L).2 let h_splits : g1.length = dim ∧ g2.length = dim := split_at_lengths_gen dim dim L h let h_equal : g1.length = g2.length := Eq.trans h_splits.left (Eq.symm h_splits.right) let h1_new := List.zipWith (fun a b => sa.mul (sa.add a b) sa.scale) g1 g2 let h2_new := List.zipWith (fun a b => sa.mul (sa.sub b a) sa.scale) g1 g2 let h_h1_new_len : h1_new.length = dim := Eq.trans (length_zipWith (fun a b => sa.mul (sa.add a b) sa.scale) g1 g2 h_equal) h_splits.left let h_h2_new_len : h2_new.length = dim := Eq.trans (length_zipWith (fun a b => sa.mul (sa.sub b a) sa.scale) g1 g2 h_equal) h_splits.left Eq.trans (length_append h1_new h2_new) (congr_add h_h1_new_len h_h2_new_len) theorem split_at_forwardCore (sa : ScaleAlgebra F) (dim : Nat) (L : List F) (h : L.length = dim + dim) : split_at dim (forwardCore sa dim L) = (List.zipWith (fun a b => sa.mul (sa.add a b) sa.scale) (split_at dim L).1 (split_at dim L).2, List.zipWith (fun a b => sa.mul (sa.sub b a) sa.scale) (split_at dim L).1 (split_at dim L).2) := let g1 := (split_at dim L).1 let g2 := (split_at dim L).2 let h_splits : g1.length = dim ∧ g2.length = dim := split_at_lengths_gen dim dim L h let h_equal : g1.length = g2.length := Eq.trans h_splits.left (Eq.symm h_splits.right) let h1_new := List.zipWith (fun a b => sa.mul (sa.add a b) sa.scale) g1 g2 let h_len : h1_new.length = dim := Eq.trans (length_zipWith (fun a b => sa.mul (sa.add a b) sa.scale) g1 g2 h_equal) h_splits.left split_at_append dim h1_new (List.zipWith (fun a b => sa.mul (sa.sub b a) sa.scale) g1 g2) h_len def ValidShape : List Nat → Prop | [] => False | [x] => x > 0 | x :: xs => x > 0 ∧ ValidShape xs def shapeProd : List Nat → Nat | [] => 1 | x :: xs => x * shapeProd xs structure Tensor (F : Type) where shape : List Nat data : List F h_valid : ValidShape shape h_len : data.length = shapeProd shape def init_tensor_spec (F : Type) (shape : List Nat) (data : List F) : Prop := ValidShape shape ∧ data.length = shapeProd shape theorem tensor_init_rejects_invalid_shape (shape : List Nat) (h_invalid : ¬ ValidShape shape) : (d : List F) → ¬ init_tensor_spec F shape d := fun _ h_spec => h_invalid h_spec.left theorem valid_shape_empty_is_false : ¬ ValidShape [] := fun h => h theorem valid_shape_zero_is_false : (xs : List Nat) → ¬ ValidShape (0 :: xs) | [] => fun h => Nat.lt_irrefl 0 h | _ :: _ => fun h => Nat.lt_irrefl 0 h.left def usize_max : Nat := 18446744073709551615 def ValidDim (dim : Nat) : Prop := dim > 0 ∧ dim ≤ usize_max / 2 def ValidLen (dim : Nat) (n : Nat) : Prop := n = dim + dim def transform_precondition (dim : Nat) (L : List F) : Prop := ValidDim dim ∧ L.length = dim + dim theorem transform_mismatched_size (dim : Nat) (L : List F) (h_mismatch : L.length ≠ dim + dim) : ¬ transform_precondition dim L := fun h => h_mismatch h.right def mixForwardCore (sa : ScaleAlgebra F) (dim : Nat) (L : List F) (_ : transform_precondition dim L) : List F := forwardCore sa dim L theorem forwardCore_not_injective (sa : ScaleAlgebra F) : ∃ L1 L2 : List F, L1 ≠ L2 ∧ forwardCore sa 1 L1 = forwardCore sa 1 L2 := by obtain ⟨a, b, hab⟩ := sa.exists_distinct refine ⟨[a], [b], ?_, ?_⟩ · intro h cases h exact hab rfl · rfl frissísd úgy hogy P, Q ∈ ℂ[x, y] are polynomials (finitely many terms, no roots, negative exponents, exp, log, fractions, or power series). teljes kodot komment nelkul kuldod vissza a kert frissitessel es semmi mast nem kuldesz