examples.lean

import tactic data.stream.basic data.set.basic data.finset data.multiset
       category.traversable.derive meta.coinductive_predicates

open tactic

universe u
variable {α : Type}

example (s t u : set ℕ) (h : s ⊆ t ∩ u) (h' : u ⊆ s) : u ⊆ s → true :=
begin
  dunfold has_subset.subset has_inter.inter at *,
--  trace_state,
  intro1, triv
end

example (s t u : set ℕ) (h : s ⊆ t ∩ u) (h' : u ⊆ s) : u ⊆ s → true :=
begin
  delta has_subset.subset has_inter.inter at *,
--  trace_state,
  intro1, triv
end

example (x y z : ℕ) (h'' : true) (h : 0 + y = x) (h' : 0 + y = z) : x = z + 0 :=
begin
  simp at *,
--  trace_state,
  rw [←h, ←h']
end

example (x y z : ℕ) (h'' : true) (h : 0 + y = x) (h' : 0 + y = z) : x = z + 0 :=
begin
  simp at *,
  simp [h] at h',
  simp [*]
end

def my_id (x : α) := x

def my_id_def (x : α) : my_id x = x := rfl

example (x y z : ℕ) (h'' : true) (h : 0 + my_id y = x) (h' : 0 + y = z) : x = z + 0 :=
begin
  simp [my_id_def] at *, simp [h] at h', simp [*]
end

@[simp] theorem mem_set_of {a : α} {p : α → Prop} : a ∈ {a | p a} = p a := rfl

-- TODO: write a tactic to unfold specific instances of generic notation?
theorem subset_def {s t : set α} : (s ⊆ t) = ∀ x, x ∈ s → x ∈ t := rfl
theorem union_def {s₁ s₂ : set α} : s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂} := rfl
theorem inter_def {s₁ s₂ : set α} : s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂} := rfl

theorem union_subset {s t r : set α} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ t ⊆ r :=
begin
  dsimp [subset_def, union_def] at *,
  intros x h,
  cases h; back_chaining_using_hs
end

theorem subset_inter {s t r : set α} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩ t :=
begin
  dsimp [subset_def, inter_def] at *,
  intros x h,
  split; back_chaining_using_hs
end

/- extensionality -/

example : true :=
begin
  have : ∀ (s₀ s₁ : set ℤ), s₀ = s₁,
  { intros, ext1,
    guard_target x ∈ s₀ ↔ x ∈ s₁,
    admit },
  have : ∀ (s₀ s₁ : finset ℕ), s₀ = s₁,
  { intros, ext1,
    guard_target a ∈ s₀ ↔ a ∈ s₁,
    admit },
  have : ∀ (s₀ s₁ : multiset ℕ), s₀ = s₁,
  { intros, ext1,
    guard_target multiset.count a s₀ = multiset.count a s₁,
    admit },
  have : ∀ (s₀ s₁ : list ℕ), s₀ = s₁,
  { intros, ext1,
    guard_target list.nth s₀ n = list.nth s₁ n,
    admit },
  have : ∀ (s₀ s₁ : stream ℕ), s₀ = s₁,
  { intros, ext1,
    guard_target stream.nth n s₀ = stream.nth n s₁,
    admit },
  have : ∀ n (s₀ s₁ : array n ℕ), s₀ = s₁,
  { intros, ext1,
    guard_target array.read s₀ i = array.read s₁ i,
    admit },
  trivial
end

/- choice -/
example (h : ∀n m : ℕ, ∃i j, m = n + i ∨ m + j = n) : true :=
begin
  choose i j h using h,
  guard_hyp i := ℕ → ℕ → ℕ,
  guard_hyp j := ℕ → ℕ → ℕ,
  guard_hyp h := ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n,
  trivial
end

example (h : ∀n m : ℕ, ∃i, ∀n:ℕ, ∃j, m = n + i ∨ m + j = n) : true :=
begin
  choose i j h using h,
  guard_hyp i := ℕ → ℕ → ℕ,
  guard_hyp j := ℕ → ℕ → ℕ → ℕ,
  guard_hyp h := ∀ (n m k : ℕ), m = k + i n m ∨ m + j n m k = k,
  trivial
end

-- Test `simp only [exists_prop]` gets applied after choosing.
-- Because of this simp, we need a non-rfl goal
example (h : ∀ n, ∃ k ≥ 0, n = k) : ∀ x : ℕ, 1 = 1 :=
begin
  choose u hu using h,
  guard_hyp hu := ∀ n, u n ≥ 0 ∧ n = u n,
  intro, refl
end

/- refine_struct -/
section refine_struct

variables {α} [_inst : monoid α]
include _inst

example : true :=
begin
  have : group α,
  { refine_struct { .._inst },
    guard_tags _field inv group, admit,
    guard_tags _field mul_left_inv group, admit, },
  trivial
end

end refine_struct

meta example : true :=
begin
   success_if_fail { let := compact_relation },
   trivial
end

import_private compact_relation from tactic.coinduction

meta example : true :=
begin
  let := compact_relation,
  trivial
end

meta example : true :=
begin
   success_if_fail { let := elim_gen_sum_aux },
   trivial
end

import_private elim_gen_sum_aux

meta example : true :=
begin
  let := elim_gen_sum_aux,
  trivial
end

/- traversable -/
open tactic.interactive

run_cmd do
lawful_traversable_derive_handler' `test ``(is_lawful_traversable) ``list
-- the above creates local instances of `traversable` and `is_lawful_traversable`
-- for `list`
-- do not put in instances because they are not universe polymorphic

@[derive [traversable, is_lawful_traversable]]
structure my_struct (α : Type) :=
  (y : ℤ)

@[derive [traversable, is_lawful_traversable]]
inductive either (α : Type u)
| left : α → ℤ → either
| right : α → either

@[derive [traversable, is_lawful_traversable]]
structure my_struct2 (α : Type u) : Type u :=
  (x : α)
  (y : ℤ)
  (η : list α)
  (k : list (list α))

@[derive [traversable, is_lawful_traversable]]
inductive rec_data3 (α : Type u) : Type u
| nil : rec_data3
| cons : ℕ → α → rec_data3 → rec_data3 → rec_data3

@[derive traversable]
meta structure meta_struct (α : Type u) : Type u :=
  (x : α)
  (y : ℤ)
  (z : list α)
  (k : list (list α))
  (w : expr)

/- tests of has_sep on finset -/


example {α} (s : finset α) (p : α → Prop) [decidable_pred p] : {x ∈ s | p x} = s.filter p :=
by simp

example {α} (s : finset α) (p : α → Prop) [decidable_pred p] :
  {x ∈ s | p x} = @finset.filter α p (λ _, classical.prop_decidable _) s :=
by simp

section
open_locale classical

example {α} (s : finset α) (p : α → Prop) : {x ∈ s | p x} = s.filter p :=
by simp

example (n m k : ℕ) : {x ∈ finset.range n | x < m ∨ x < k } =
  {x ∈ finset.range n | x < m } ∪ {x ∈ finset.range n | x < k } :=
by simp [finset.filter_or]

end