generalize_proofs

Stream: general

[Reid Barton]

Does generalize_proofs ever work?

[Reid Barton]

I get this error unknown declaration '1'

[Simon Hudon]

What did you write?

[Simon Hudon]

I think generalize_proofs is obsolete. I remember @Mario Carneiro saying that h_generalize does the work generalize_proofs was intended to do

[Reid Barton]

something very complicated

[Reid Barton]

ah, let me try that

[Reid Barton]

hmm, I realized I need to also generalize the type that it is being converted to, and that seems tricky

[Reid Barton]

I'll just go back to my interim solution

[Simon Hudon]

Try h_generalize! h : my_var == new_name then you can generalize the type of the new variable

[Chris Hughes]

Does changing the definition of collect_proofs_in in tactic.generalize_proofs to this work?

private meta def collect_proofs_in :
  expr → list expr → list name × list expr → tactic (list name × list expr)
| e ctx (ns, hs) :=
let go (tac : list name × list expr → tactic (list name × list expr)) :
  tactic (list name × list expr) :=
(do t ← infer_type e,
   mcond (is_prop t) (do
     first (hs.map $ λ h, do
       t' ← infer_type h,
       is_def_eq t t',
       g ← target,
       change $ g.replace (λ a n, if a = e then some h else none),
       return (ns, hs)) <|>
     (let (n, ns) := (match ns with
        | [] := (`_x, [])
        | (n :: ns) := (n, ns)
        end : name × list name) in
      do generalize e n,
         h ← intro n,
         return (ns, h::hs)) <|> return (ns, hs)) (tac (ns, hs))) <|> return (ns, hs) in
match e with
| (expr.const _ _)   := go return
| (expr.local_const _ _ _ t) := collect_proofs_in t ctx (ns, hs)
| (expr.mvar _ _ t)  := collect_proofs_in t ctx (ns, hs)
| (expr.app f x)     :=
  go (λ nh, collect_proofs_in f ctx nh >>= collect_proofs_in x ctx)
| (expr.lam n b d e) :=
  go (λ nh, do
    nh ← collect_proofs_in d ctx nh,
    var ← mk_local' n b d,
    collect_proofs_in (expr.instantiate_var e var) (var::ctx) nh)
| (expr.pi n b d e) := do
  nh ← collect_proofs_in d ctx (ns, hs),
  var ← mk_local' n b d,
  collect_proofs_in (expr.instantiate_var e var) (var::ctx) nh
| (expr.elet n t d e) :=
  go (λ nh, do
    nh ← collect_proofs_in t ctx nh,
    nh ← collect_proofs_in d ctx nh,
    collect_proofs_in (expr.instantiate_var e d) ctx nh)
| (expr.macro m l) :=
  go (λ nh, mfoldl (λ x e, collect_proofs_in e ctx x) nh l)
| _                  := return (ns, hs)
end

[Chris Hughes]

I think the problem is that infer_type fails given a sort

[Mario Carneiro]

generalize_proofs is not so much obsolete as broken and abandoned

[Mario Carneiro]

I think it works as long as there are no binders in the goal