Recognize propositions as instances

Stream: new members

[Robert Maxton]

I'm not entirely sure how to even phrase this question properly, but... Let's say I have some arbitrary proposition, say
a = succ b, and I want to convert this into an application of a lemma, (λ y, y = succ b) a, so I can use it with the myriad theorems that expect terms of the form f a. Is there a tactic for doing this already?

[Robert Maxton]

(generalize seems close in concept but doesn't in fact do the job of making things that the unifier can recognize as of the form (a -> Prop) (a))

[Kyle Miller]

Would you mind giving a #mwe of an example where you're wanting this?

Without that, it sounds like you might want to use tactic#change, which should be able to handle this at the cost of having to write out a part of the expression.

[Robert Maxton]

change works at precisely that cost, yes, which can be particularly annoying for long expressions; I can sometimes just copy from the info view but ...

[Robert Maxton]

also, more importantly, it prevents me from writing a custom induction tactic as reliable/general as I'd prefer

[Robert Maxton]

specifically, I'm trying to write a "restricted induction" tactic that uses a specific induction axiom/set comprehension axiom

[Robert Maxton]

my current implementation is just

meta def tactic.interactive.restricted_induction (v: parse ident) (ax: parse texpr): tactic unit :=
   do {
    ctx ← tactic.local_context,
    goal ← tactic.target,
    revert [v], apply ax, split}

[Robert Maxton]

(where the first two lines are currently unused)

[Robert Maxton]

together with

axiom rca: ∀(p: nat → Prop), (p Z ∧ (∀ k, p k → p S k)) → ∀ k, p k

[Robert Maxton]

but the apply is, ah, temperamental

[Robert Maxton]

I end up having to give long elaboration hints to the compiler where I copy down the exact function p: nat → Prop I need

[Robert Maxton]

I'll update with a proper example/MWE when I re-encounter one, I refactored a bunch of my code while I was waiting to work around the problem ^.^;

[Kyle Miller]

What's "restricted induction"? Is it something that induction v using rca wouldn't let you do?

[Robert Maxton]

okay, here

example (a : nat) : ∀ (b : nat), a.le b ∨ b.le a :=
begin
  restricted_induction a rca,
end

fails with

invalid apply tactic, failed to unify
  ∀ (a b : nat), a.le b ∨ b.le a
with
  (?m_1 Z ∧ ∀ (k : nat), ?m_1 k → ?m_1 (S k)) → ∀ (k : nat), ?m_1 k
state:
⊢ ∀ (a b : nat), a.le b ∨ b.le a

[Robert Maxton]

....

[Robert Maxton]

hm.

[Robert Maxton]

It might, actually

[Robert Maxton]

The first time I read it I thought it wouldn't, but now I'm not sure why I thought that

[Robert Maxton]

hm

[Robert Maxton]

well, the empirical answer is "well, it doesn't work"

[Robert Maxton]

why remains up for debate

[Kyle Miller]

(Fyi: this is closer to a #mwe, though I had to make some guesses:

import tactic

section
setup_tactic_parser
open tactic.interactive
meta def tactic.interactive.restricted_induction (v: parse ident) (ax: parse texpr): tactic unit :=
   do {
    ctx ← tactic.local_context,
    goal ← tactic.target,
    revert [v], apply ax, split}
end

axiom rca: ∀(p: nat → Prop), (p 0 ∧ (∀ k, p k → p k.succ)) → ∀ k, p k

example (a : nat) : ∀ (b : nat), a.le b ∨ b.le a :=
begin
  restricted_induction a rca,
end

)

Sometimes refine is better than apply:

example (a : nat) : ∀ (b : nat), a.le b ∨ b.le a :=
begin
  revert a,
  refine rca _ _,

end

Changing the axiom a little makes induction work:

axiom rca: ∀(p: nat → Prop), p 0 → (∀ k, p k → p k.succ) → ∀ k, p k

example (a : nat) : ∀ (b : nat), a.le b ∨ b.le a :=
begin
  induction a using rca,
end

[Robert Maxton]

Hmmm... I'm getting "unknown declaration rca"

[Robert Maxton]

if I replace induction with restricted_induction, then it at least recognizes rca, though it complains that it doesn't unify

[Robert Maxton]

ah, I was missing a namespace inclusion. Okay, that works now. Thanks!