add support for Lean Theorem Prover

samples/Lean/binary.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.binary
+Authors: Leonardo de Moura, Jeremy Avigad
+
+General properties of binary operations.
+-/
+
+import logic.eq
+open eq.ops
+
+namespace binary
+  section
+    variable {A : Type}
+    variables (op₁ : A → A → A) (inv : A → A) (one : A)
+
+    local notation a * b := op₁ a b
+    local notation a ⁻¹  := inv a
+    local notation 1     := one
+
+    definition commutative := ∀a b, a * b = b * a
+    definition associative := ∀a b c, (a * b) * c = a * (b * c)
+    definition left_identity := ∀a, 1 * a = a
+    definition right_identity := ∀a, a * 1 = a
+    definition left_inverse := ∀a, a⁻¹ * a = 1
+    definition right_inverse := ∀a, a * a⁻¹ = 1
+    definition left_cancelative := ∀a b c, a * b = a * c → b = c
+    definition right_cancelative := ∀a b c, a * b = c * b → a = c
+
+    definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) = b
+    definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) = b
+    definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b =  a
+    definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ = a
+
+    variable (op₂ : A → A → A)
+
+    local notation a + b := op₂ a b
+
+    definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c
+    definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c
+  end
+
+  context
+    variable {A : Type}
+    variable {f : A → A → A}
+    variable H_comm : commutative f
+    variable H_assoc : associative f
+    infixl `*` := f
+    theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
+    take a b c, calc
+      a*(b*c) = (a*b)*c  : H_assoc
+        ...   = (b*a)*c  : H_comm
+        ...   = b*(a*c)  : H_assoc
+
+    theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
+    take a b c, calc
+      (a*b)*c = a*(b*c) : H_assoc
+        ...   = a*(c*b) : H_comm
+        ...   = (a*c)*b : H_assoc
+  end
+
+  context
+    variable {A : Type}
+    variable {f : A → A → A}
+    variable H_assoc : associative f
+    infixl `*` := f
+    theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
+    calc
+      (a*b)*(c*d) = a*(b*(c*d)) : H_assoc
+              ... = a*((b*c)*d) : H_assoc
+  end
+
+end binary

samples/Lean/set.hlean

@@ -0,0 +1,70 @@
+-- Copyright (c) 2015 Jakob von Raumer. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Jakob von Raumer
+-- Category of sets
+
+import .basic types.pi trunc
+
+open truncation sigma sigma.ops pi function eq morphism precategory
+open equiv
+
+namespace precategory
+
+  universe variable l
+
+  definition set_precategory : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A) :=
+  begin
+    fapply precategory.mk.{l+1 l},
+                  intros, apply (a.1 → a_1.1),
+                intros, apply trunc_pi, intros, apply b.2,
+              intros, intro x, exact (a_1 (a_2 x)),
+            intros, exact (λ (x : a.1), x),
+          intros, apply funext.path_pi, intro x, apply idp,
+        intros, apply funext.path_pi, intro x, apply idp,
+      intros, apply funext.path_pi, intro x, apply idp,
+  end
+
+end precategory
+
+namespace category
+
+  universe variable l
+  local attribute precategory.set_precategory.{l+1 l} [instance]
+
+  definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A))
+    : (a ≅ b) = (a.1 ≃ b.1) :=
+  /-begin
+    apply ua, fapply equiv.mk,
+      intro H,
+        apply (isomorphic.rec_on H), intros (H1, H2),
+        apply (is_iso.rec_on H2), intros (H3, H4, H5),
+        fapply equiv.mk,
+        apply (isomorphic.rec_on H), intros (H1, H2),
+        exact H1,
+      fapply is_equiv.adjointify, exact H3,
+          exact sorry,
+        exact sorry,
+  end-/ sorry
+
+  definition set_category : category.{l+1 l} (Σ (A : Type.{l}), is_hset A) :=
+  /-begin
+    assert (C : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A)),
+      apply precategory.set_precategory,
+    apply category.mk,
+    assert (p : (λ A B p, (set_category_equiv_iso A B) ▹ iso_of_path p) = (λ A B p, @equiv_path A.1 B.1 p)),
+    apply is_equiv.adjointify,
+        intros,
+        apply (isomorphic.rec_on a_1), intros (iso', is_iso'),
+        apply (is_iso.rec_on is_iso'), intros (f', f'sect, f'retr),
+        fapply sigma.path,
+          apply ua, fapply equiv.mk, exact iso',
+          fapply is_equiv.adjointify,
+              exact f',
+            intros, apply (f'retr ▹ _),
+          intros, apply (f'sect ▹ _),
+        apply (@is_hprop.elim),
+        apply is_trunc_is_hprop,
+      intros,
+  end -/ sorry
+
+end category