[WIP] added a co_cases tactic for manipulating the inner

representation of coinductive types.

Not meant for manipulating individual coinductive types

data/coinductive.lean → data/coinductive/basic.lean

@@ -647,7 +647,7 @@ end
 
 variables {β}
 
-lemma coinduction {s₁ s₂ : cofix β}
+lemma coinduction (s₁ s₂ : cofix β)
   (hh : head s₁ = head s₂)
   (ht : ∀ (FR : cofix β → cofix β → Prop),
           reflexive FR →
@@ -679,7 +679,7 @@ def corec_on {X : Type*} (x₀ : X) (f : X → (Σ (y : α), β y → X)) : cofi
 cofix.corec f x₀
 
 theorem corec_eq {X : Type*} (f : X → (Σ (y : α), β y → X)) (x₀ : X)
-: cofix.corec f x₀ = sigma.rec_on (f x₀) (λ y ch, cofix.mk y (λ i, cofix.corec f (ch i))) :=
+: cofix.corec f x₀ = cofix.mk (f x₀).1 (λ i, cofix.corec f ((f x₀).2 i)) :=
 begin
   cases Hf : f x₀, simp,
   apply coinduction,

data/coinductive/default.lean

@@ -0,0 +1,3 @@
+
+import .basic
+import .tactic

data/coinductive/examples.lean

@@ -151,4 +151,11 @@ instance {α} [has_repr α] : has_repr (bin_tree α) :=
 (node 0 (node (node 1 (node 1 (node (node 2 ⊥) (node 3 ⊥))))
               (node 2 (node 2 (node (node 3 ⊥) (node 4 ⊥))))))
 -/
+
+example {A} (p q : l_two_tree_intl A) : p = q :=
+begin
+  co_cases p,
+  admit
+end
+
 end examples

data/coinductive/tactic.lean

@@ -0,0 +1,36 @@
+import .basic
+#check @cofix.cases
+namespace tactic
+open lean.parser interactive interactive.types
+open tactic.interactive (generalize cases_arg_p)
+local postfix `?`:9000 := optional
+
+meta def lambdas : list expr → expr → tactic expr
+| (v@(expr.local_const uniq pp info _) :: es) f := do
+  t ← infer_type v,
+  f' ← lambdas es f,
+  return $ expr.lam pp info t $ expr.abstract_local f' uniq
+| _ f := return f
+
+meta def co_cases (pat : parse cases_arg_p) (ns : parse with_ident_list) : tactic unit :=
+do ls ← local_context,
+   e ← to_expr pat.2,
+   ls ← ls.mfilter (λ h, do
+     t ← infer_type h,
+     return $ e.occurs t),
+   n ← revert_lst ls,
+   generalize e `p,
+   p ← intro1,
+   t ← target,
+   lam ← lambdas [p] t,
+   refine ``(@cofix.cases _ _ %%lam _ %%p),
+   clear p,
+   when (e.is_local_constant ∧ pat.1.is_none) (clear e),
+   intro_lst $ ns.take 2,
+   intron (2 - ns.length),
+   target >>= head_beta >>= change,
+   intron n
+
+run_cmd add_interactive [`co_cases]
+
+end tactic