You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Aug 24, 2024. It is now read-only.
"/-|\nCopyright (c) 2014 Microsoft Corporation. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthor: Leonardo de Moura, Jeremy Avigad, Haitao Zhang\n|-/\n-- a port of core Lean `init/function.lean`\n\n/-!\n# General operations on functions\n-/\n\nnamespace Function\n\nvariable {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁}\n\n@[reducible] def comp_right (f : β → β → β) (g : α → β) : β → α → β :=\nλ b a => f b (g a)\n\n@[reducible] def comp_left (f : β → β → β) (g : α → β) : α → β → β :=\nλ a b => f (g a) b\n\n/-- Given functions `f : β → β → φ` and `g : α → β`, produce a function `α → α → φ` that evaluates\n`g` on each argument, then applies `f` to the results. Can be used, e.g., to transfer a relation\nfrom `β` to `α`. -/\n@[reducible] def on_fun (f : β → β → φ) (g : α → β) : α → α → φ :=\nλ x y => f (g x) (g y)\n\n@[reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ)\n : α → β → ζ :=\nλ x y => op (f x y) (g x y)\n\n@[reducible] def swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y :=\nλ y x => f x y\n\n@[reducible] def app {β : α → Sort u₂} (f : ∀ x, β x) (x : α) : β x :=\nf x\n\ntheorem left_id (f : α → β) : id ∘ f = f := rfl\n\ntheorem right_id (f : α → β) : f ∘ id = f := rfl\n\n@[simp] theorem comp_app (f : β → φ) (g : α → β) (a : α) : (f ∘ g) a = f (g a) := rfl\n\ntheorem comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl\n\n@[simp] theorem comp.left_id (f : α → β) : id ∘ f = f := rfl\n\n@[simp] theorem comp.right_id (f : α → β) : f ∘ id = f := rfl\n\ntheorem comp_const_right (f : β → φ) (b : β) : f ∘ (const α b) = const α (f b) := rfl\n\n/-- A function `f : α → β` is called injective if `f x = f y` implies `x = y`. -/\n@[reducible] def injective (f : α → β) : Prop := ∀ {a₁ a₂}, f a₁ = f a₂ → a₁ = a₂\n\ntheorem injective.comp {g : β → φ} {f : α → β} (hg : injective g) (hf : injective f) :\n injective (g ∘ f) :=\nλ h => hf (hg h)\n\n/-- A function `f : α → β` is calles surjective if every `b : β` is equal to `f a`\nfor some `a : α`. -/\n@[reducible] def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b\n\ntheorem surjective.comp {g : β → φ} {f : α → β} (hg : surjective g) (hf : surjective f) :\n surjective (g ∘ f) :=\nλ (c : φ) => Exists.elim (hg c) (λ b hb => Exists.elim (hf b) (λ a ha =>\n Exists.intro a (show g (f a) = c from (Eq.trans (congrArg g ha) hb))))\n\n/-- A function is called bijective if it is both injective and surjective. -/\ndef bijective (f : α → β) := injective f ∧ surjective f\n\ntheorem bijective.comp {g : β → φ} {f : α → β} : bijective g → bijective f → bijective (g ∘ f)\n| ⟨h_ginj, h_gsurj⟩, ⟨h_finj, h_fsurj⟩ => ⟨h_ginj.comp h_finj, h_gsurj.comp h_fsurj⟩\n\n/-- `left_inverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/\ndef left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x\n\n/-- `has_left_inverse f` means that `f` has an unspecified left inverse. -/\ndef has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f\n\n/-- `right_inverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/\ndef right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g\n\n/-- `has_right_inverse f` means that `f` has an unspecified right inverse. -/\ndef has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f\n\ntheorem left_inverse.injective {g : β → α} {f : α → β} : left_inverse g f → injective f :=\nλ h a b hf => h a ▸ h b ▸ hf ▸ rfl\n\ntheorem has_left_inverse.injective {f : α → β} : has_left_inverse f → injective f :=\nλ h => Exists.elim h (λ finv inv => inv.injective)\n\ntheorem right_inverse_of_injective_of_left_inverse {f : α → β} {g : β → α}\n (injf : injective f) (lfg : left_inverse f g) :\n right_inverse f g :=\nλ x => injf $ lfg $ f x\n\ntheorem right_inverse.surjective {f : α → β} {g : β → α} (h : right_inverse g f) : surjective f :=\nλ y => ⟨g y, h y⟩\n\ntheorem has_right_inverse.surjective {f : α → β} : has_right_inverse f → surjective f\n| ⟨finv, inv⟩ => inv.surjective\n\ntheorem left_inverse_of_surjective_of_right_inverse {f : α → β} {g : β → α} (surjf : surjective f)\n (rfg : right_inverse f g) : left_inverse f g :=\nλ y =>\n let ⟨x, hx⟩ := surjf y\n by rw [",
"import Lean\n\nopen Lean.Elab\n\nstructure A where\n val : Nat → Nat\n\nstructure B where\n pair : A × A\n\ndef f (x : Nat) : Nat × Nat :=\n let y := ⟨x, x⟩\n id y\n\ndef h : (x y : Nat) → (b : Bool) → x + 0 = x :=\n fun x y b => by\n simp\n\ndef f2 : (x y : Nat) → (b : Bool) → Nat :=\n fun x y b =>\n let (z, w) := (x + y, x - y)\n let z1 := z + w\n z + z1\n\ndef f3 (s : Nat × Array (Array Nat)) : Array Nat :=\n s.2[1].push s.1\n\ndef f4 (arg : B) : Nat :=\n arg.pair.fst.val 0\n\ndef f5 (x : Nat) : B := {\n pair := ({ val := id }, { val := id })\n}\n\nopen Nat in\n",
2
+
"import Lean\n\nopen Lean.Elab\n\nstructure A where\n val : Nat → Nat\n\nstructure B where\n pair : A × A\n\ndef f (x : Nat) : Nat × Nat :=\n let y := ⟨x, x⟩\n id y\n\ndef h : (x y : Nat) → (b : Bool) → x + 0 = x :=\n fun x y b => ",
[{"contents": "infoTree.lean:39:0: error: expected identifier or term\n",
19
-
"_type": "message"},
20
-
{"contents": "infoTree.lean:39:5: error: unexpected end of input\n",
21
-
"_type": "message"}],
22
-
"goals": [],
23
-
"contents": "",
24
-
"_type": "sentence"}]
18
+
{"contents":
19
+
"\n\ndef f2 : (x y : Nat) → (b : Bool) → Nat :=\n fun x y b =>\n let (z, w) := (x + y, x - y)\n let z1 := z + w\n z + z1\n\ndef f3 (s : Nat × Array (Array Nat)) : Array Nat :=\n s.2[1].push s.1\n\ndef f4 (arg : B) : Nat :=\n arg.pair.fst.val 0\n\ndef f5 (x : Nat) : B := {\n pair := ({ val := id }, { val := id })\n}\n\nopen Nat in\n",
0 commit comments