feat(category/applicative): id and comp functors; proofs by norm (

#184)

category/applicative.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2017 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+
+Instances for identity and composition functors
+-/
+
+import category.functor
+
+universe variables u v w
+
+section lemmas
+
+open function
+
+variables {f : Type u → Type v}
+variables [applicative f] [is_lawful_applicative f]
+variables {α β γ σ : Type u}
+
+attribute [functor_norm] seq_assoc pure_seq_eq_map map_pure seq_map_assoc map_seq
+
+lemma applicative.map_seq_map (g : α → β → γ) (h : σ → β) (x : f α) (y : f σ) :
+  (g <$> x) <*> (h <$> y) = (flip (∘) h ∘ g) <$> x <*> y :=
+by simp [flip] with functor_norm
+
+lemma applicative.pure_seq_eq_map' (g : α → β) :
+  (<*>) (pure g : f (α → β)) = (<$>) g :=
+by ext; simp with functor_norm
+
+end lemmas
+
+namespace comp
+
+open function (hiding comp)
+open functor
+
+variables {f : Type u → Type w} {g : Type v → Type u}
+
+variables [applicative f] [applicative g]
+
+protected def seq  {α β : Type v} : comp f g (α → β) → comp f g α → comp f g β
+| ⟨h⟩ ⟨x⟩ := ⟨has_seq.seq <$> h <*> x⟩
+
+instance : has_pure (comp f g) :=
+⟨λ _ x, ⟨pure $ pure x⟩⟩
+
+instance : has_seq (comp f g) :=
+⟨λ _ _ f x, comp.seq f x⟩
+
+@[simp]
+protected lemma run_pure {α : Type v} :
+  ∀ x : α, (pure x : comp f g α).run = pure (pure x)
+| _ := rfl
+
+@[simp]
+protected lemma run_seq {α β : Type v} :
+  ∀ (h : comp f g (α → β)) (x : comp f g α),
+  (h <*> x).run = (<*>) <$> h.run <*> x.run
+| ⟨_⟩ ⟨_⟩ := rfl
+
+variables [is_lawful_applicative f] [is_lawful_applicative g]
+variables {α β γ : Type v}
+
+lemma map_pure (h : α → β) (x : α) : (h <$> pure x : comp f g β) = pure (h x) :=
+by ext; simp
+
+lemma seq_pure (h : comp f g (α → β)) (x : α) :
+  h <*> pure x = (λ g : α → β, g x) <$> h :=
+by ext; simp [(∘)] with functor_norm
+
+lemma seq_assoc (x : comp f g α) (h₀ : comp f g (α → β)) (h₁ : comp f g (β → γ)) :
+   h₁ <*> (h₀ <*> x) = (@function.comp α β γ <$> h₁) <*> h₀ <*> x :=
+by ext; simp [(∘)] with functor_norm
+
+lemma pure_seq_eq_map (h : α → β)  (x : comp f g α) :
+  pure h <*> x = h <$> x :=
+by ext; simp [applicative.pure_seq_eq_map'] with functor_norm
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [applicative f] [applicative g] :
+  applicative (comp f g) :=
+{ map := @comp.map f g _ _,
+  seq := @comp.seq f g _ _,
+  ..comp.has_pure }
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [applicative f] [applicative g]
+  [is_lawful_applicative f] [is_lawful_applicative g] :
+  is_lawful_applicative (comp f g) :=
+{ pure_seq_eq_map := @comp.pure_seq_eq_map f g _ _ _ _,
+  map_pure := @comp.map_pure f g _ _ _ _,
+  seq_pure := @comp.seq_pure f g _ _ _ _,
+  seq_assoc := @comp.seq_assoc f g _ _ _ _ }
+
+end comp
+open functor
+
+@[functor_norm]
+lemma comp.seq_mk {α β : Type w}
+  {f : Type u → Type v} {g : Type w → Type u}
+  [applicative f] [applicative g]
+  (h : f (g (α → β))) (x : f (g α)) :
+  comp.mk h <*> comp.mk x = comp.mk (has_seq.seq <$> h <*> x) := rfl

category/basic.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 Extends the theory on functors, applicatives and monads.
 -/
 
-universes u v w x y
+universes u v
 variables {α β γ : Type u}
 
 notation a ` $< `:1 f:1 := f a
@@ -16,7 +16,7 @@ variables {f : Type u → Type v} [functor f] [is_lawful_functor f]
 
 run_cmd mk_simp_attr `functor_norm
 
-@[functor_norm] theorem map_map (m : α → β) (g : β → γ) (x : f α) :
+@[functor_norm] protected theorem map_map (m : α → β) (g : β → γ) (x : f α) :
   g <$> (m <$> x) = (g ∘ m) <$> x :=
 (comp_map _ _ _).symm
 
@@ -25,13 +25,31 @@ run_cmd mk_simp_attr `functor_norm
 end functor
 
 section applicative
-variables {f : Type u → Type v} [applicative f] [is_lawful_applicative f]
+variables {f : Type u → Type v} [applicative f]
+
+def mzip_with
+  {α₁ α₂ φ : Type u}
+  (g : α₁ → α₂ → f φ) :
+  Π (ma₁ : list α₁) (ma₂: list α₂), f (list φ)
+| (x :: xs) (y :: ys) := (::) <$> g x y <*> mzip_with xs ys
+| _ _ := pure []
+
+def mzip_with'  (g : α → β → f γ) : list α → list β → f punit
+| (x :: xs) (y :: ys) := g x y *> mzip_with' xs ys
+| [] _ := pure punit.star
+| _ [] := pure punit.star
+
+variables [is_lawful_applicative f]
 
 attribute [functor_norm] seq_assoc pure_seq_eq_map
 
 @[simp] theorem pure_id'_seq (x : f α) : pure (λx, x) <*> x = x :=
 pure_id_seq x
 
+variables  [is_lawful_applicative f]
+
+attribute [functor_norm] seq_assoc pure_seq_eq_map
+
 @[functor_norm] theorem seq_map_assoc (x : f (α → β)) (g : γ → α) (y : f γ) :
   (x <*> (g <$> y)) = (λ(m:α→β), m ∘ g) <$> x <*> y :=
 begin
@@ -51,7 +69,7 @@ section monad
 variables {m : Type u → Type v} [monad m] [is_lawful_monad m]
 
 lemma map_bind (x : m α) {g : α → m β} {f : β → γ} : f <$> (x >>= g) = (x >>= λa, f <$> g a) :=
-by simp [bind_assoc, (∘), (bind_pure_comp_eq_map _ _ _).symm]
+by rw [← bind_pure_comp_eq_map,bind_assoc]; simp [bind_pure_comp_eq_map]
 
 lemma seq_bind_eq (x : m α) {g : β → m γ} {f : α → β} : (f <$> x) >>= g = (x >>= g ∘ f) :=
 show bind (f <$> x) g = bind x (g ∘ f),
@@ -85,10 +103,3 @@ calc f <$> a <*> b = (λp:α×β, f p.1 p.2) <$> (prod.mk <$> a <*> b) :
   ... = (λb a, f a b) <$> b <*> a :
     by rw [is_comm_applicative.commutative_prod];
         simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map]
-
-def mmap₂
-  {α₁ α₂ φ : Type u} {m : Type u → Type*} [applicative m]
-  (f : α₁ → α₂ → m φ)
-: Π (ma₁ : list α₁) (ma₂: list α₂), m (list φ)
- | (x :: xs) (y :: ys) := (::) <$> f x y <*> mmap₂ xs ys
- | _ _ := pure []

category/functor.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2017 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+
+Standard identity and composition functors
+-/
+import tactic.ext
+import category.basic
+
+universe variables u v w
+
+section functor
+
+variables {F : Type u → Type v}
+variables {α β γ : Type u}
+variables [functor F] [is_lawful_functor F]
+
+lemma functor.map_id : (<$>) id = (id : F α → F α) :=
+by apply funext; apply id_map
+
+lemma functor.map_comp_map (f : α → β) (g : β → γ) :
+  ((<$>) g ∘ (<$>) f : F α → F γ) = (<$>) (g ∘ f) :=
+by apply funext; intro; rw comp_map
+
+end functor
+
+def id.mk {α : Sort u} : α → id α := id
+
+namespace functor
+
+/-- `functor.comp` is a wrapper around `function.comp` for types.
+    It prevents Lean's type class resolution mechanism from trying
+    a `functor (comp f id)` when `functor f` would do. -/
+structure comp (f : Type u → Type w) (g : Type v → Type u) (α : Type v) : Type w :=
+(run : f $ g α)
+
+@[extensionality]
+protected lemma comp.ext {f : Type u → Type w} {g : Type v → Type u} {α : Type v} :
+  ∀ {x y : comp f g α}, x.run = y.run → x = y
+| ⟨x⟩ ⟨._⟩ rfl := rfl
+
+namespace comp
+
+variables {f : Type u → Type w} {g : Type v → Type u}
+
+variables [functor f] [functor g]
+
+protected def map {α β : Type v} (h : α → β) : comp f g α → comp f g β
+| ⟨x⟩ := ⟨(<$>) h <$> x⟩
+
+variables [is_lawful_functor f] [is_lawful_functor g]
+variables {α β γ : Type v}
+
+protected lemma id_map : ∀ (x : comp f g α), comp.map id x = x
+| ⟨x⟩ :=
+by simp [comp.map,functor.map_id]
+
+protected lemma comp_map (g_1 : α → β) (h : β → γ) : ∀ (x : comp f g α),
+           comp.map (h ∘ g_1) x = comp.map h (comp.map g_1 x)
+| ⟨x⟩ :=
+by simp [comp.map,functor.map_comp_map g_1 h] with functor_norm
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [functor f] [functor g] :
+  functor (comp f g) :=
+{ map := @comp.map f g _ _ }
+
+@[simp]
+protected lemma run_map {α β : Type v} (h : α → β) :
+  ∀ x : comp f g α, (h <$> x).run = (<$>) h <$> x.run
+| ⟨_⟩ := rfl
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [functor f] [functor g]
+  [is_lawful_functor f] [is_lawful_functor g] :
+  is_lawful_functor (comp f g) :=
+{ id_map := @comp.id_map f g _ _ _ _,
+  comp_map := @comp.comp_map f g _ _ _ _ }
+
+end comp
+
+@[functor_norm]
+lemma comp.map_mk {α β : Type w}
+  {f : Type u → Type v} {g : Type w → Type u}
+  [functor f] [functor g]
+  (h : α → β) (x : f (g α)) :
+  h <$> comp.mk x = comp.mk ((<$>) h <$> x) := rfl
+
+end functor
+
+namespace ulift
+
+instance : functor ulift :=
+{ map := λ α β f, up ∘ f ∘ down }
+
+end ulift
+
+namespace sum
+
+variables {γ α β : Type v}
+
+protected def mapr (f : α → β) : γ ⊕ α → γ ⊕ β
+| (inl x) := inl x
+| (inr x) := inr (f x)
+
+instance : functor (sum γ) :=
+{ map := @sum.mapr γ }
+
+instance : is_lawful_functor.{v} (sum γ) :=
+{ id_map := by intros; casesm _ ⊕ _; refl,
+  comp_map := by intros; casesm _ ⊕ _; refl }
+
+end sum

data/prod.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 
 Extends theory on products
 -/
+import tactic.ext
 
 universes u v
 variables {α : Type u} {β : Type v}
@@ -23,6 +24,7 @@ namespace prod
 lemma ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 :=
 by rw [← @mk.eta _ _ p, ← @mk.eta _ _ q, mk.inj_iff]
 
+@[extensionality]
 lemma ext {α β} {p q : α × β} : p.1 = q.1 → p.2 = q.2 → p = q :=
 by rw [ext_iff] ; intros ; split ; assumption
 
@@ -60,4 +62,3 @@ theorem lex_def (r : α → α → Prop) (s : β → β → Prop)
  end⟩
 
 end prod
-

data/set/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Leonardo de Moura
 -/
-import tactic tactic.finish data.subtype
+import tactic.ext tactic.finish data.subtype
 open function
 
 namespace set

tactic/ext.lean

@@ -0,0 +1,75 @@
+
+import tactic.basic
+
+/--
+ Tag lemmas of the form:
+
+ ```
+ lemma my_collection.ext (a b : my_collection)
+   (h : ∀ x, a.lookup x = b.lookup y) :
+   a = b := ...
+ ```
+ -/
+@[user_attribute]
+meta def extensional_attribute : user_attribute :=
+{ name := `extensionality,
+  descr := "lemmas usable by `ext` tactic" }
+
+attribute [extensionality] _root_.funext array.ext
+
+namespace tactic
+open interactive interactive.types
+open lean.parser nat
+
+local postfix `?`:9001 := optional
+local postfix *:9001 := many
+
+/--
+  `ext1 id` selects and apply one extensionality lemma (with attribute
+  `extensionality`), using `id`, if provided, to name a local constant
+  introduced by the lemma. If `id` is omitted, the local constant is
+  named automatically, as per `intro`.
+ -/
+meta def interactive.ext1 (x : parse ident_ ?) : tactic unit :=
+do ls ← attribute.get_instances `extensionality,
+   ls.any_of (λ l, applyc l) <|> fail "no applicable extensionality rule found",
+   try ( interactive.intro x )
+
+meta def ext_arg :=
+prod.mk <$> (some <$> small_nat)
+        <*> (tk "with" *> ident_* <|> pure [])
+<|> prod.mk none <$> (ident_*)
+
+/--
+  - `ext` applies as many extensionality lemmas as possible;
+  - `ext ids`, with `ids` a list of identifiers, finds extentionality and applies them
+    until it runs out of identifiers in `ids` to name the local constants.
+
+  When trying to prove:
+
+  ```
+  α β : Type,
+  f g : α → set β
+  ⊢ f = g
+  ```
+
+  applying `ext x y` yields:
+
+  ```
+  α β : Type,
+  f g : α → set β,
+  x : α,
+  y : β
+  ⊢ y ∈ f x ↔ y ∈ f x
+  ```
+
+  by applying functional extensionality and set extensionality.
+
+  A maximum depth can be provided with `ext 3 with x y z`.
+  -/
+meta def interactive.ext : parse ext_arg → tactic unit
+ | (some n, []) := interactive.ext1 none >> iterate_at_most (pred n) (interactive.ext1 none)
+ | (none,   []) := interactive.ext1 none >> repeat (interactive.ext1 none)
+ | (n, xs) := tactic.ext xs n
+
+end tactic