Zulip Chat Archive

Stream: general

Topic: conv example


view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:43):

I was trying to write an example to illustrate the power of conv, by finding an example where the entire goal was difficult to work with because it contained implicit proofs. I realised that there were two things I didn't understand properly. Here's some code.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:43):

@[elab_simple] def subtypeadd {m : ℕ} {n : ℕ} (A : fin m) (B : fin n) : fin (m+n) :=
  ⟨A.val+B.val,add_lt_add A.is_lt B.is_lt⟩

definition phi {m n : ℕ} : fin (m + n) → fin (n + m) := λ ⟨i,Hi⟩, ⟨i,add_comm m n ▸ Hi⟩

example {m n : ℕ} (A : fin m) (B : fin n) : phi (subtypeadd A B) = subtypeadd B A :=
begin
  have H : A.val + B.val = B.val + A.val := add_comm _ _,
  -- unfold subtypeadd using show
  show phi ⟨A.val + B.val, _⟩ = ⟨B.val + A.val, _⟩,
  rw H -- fails
end

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:44):

I wanted to make the example hard for one reason, but it somehow turned out to be hard for another reason :-/

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:45):

My first question is why does the show command succeed? I assumed that what show X did was that it first checked that X made sense, and then checked that it was defeq to the goal.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:45):

But I thought I had explicitly rigged it here so that X wouldn't be able to be elaborated, because of the missing proofs.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:46):

My second question is why does rw fail. I have heard rumours that rw will not work inside a lambda (although I don't really understand why -- why is this?) but this is not a lambda and I think the reason for failure is something else.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:47):

The error message is

rewrite tactic failed, motive is not type correct
nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)
state:
m n : ℕ,
A : fin m,
B : fin n,
H : A.val + B.val = B.val + A.val
⊢ phi ⟨A.val + B.val, _⟩ = ⟨B.val + A.val, _⟩

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:47):

and if I set_option trace.check true then I get an exciting helpful extra hint:

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:47):

[check] application type mismatch at
  ⟨_a, _⟩
argument type
  A.val + B.val < m + n
expected type
  _a < m + n

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:48):

which makes no sense to me...oh! Is it rewriting too many A.val + B.val's?

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:48):

I am still a bit bewildered about why this is a type mismatch I guess.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:49):

(deleted)

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:50):

(deleted)

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 11:52):

For the first question I guess an underlying question is "which option do you switch on so you can see how Lean is filling in _s?"

view this post on Zulip Mario Carneiro (Mar 13 2018 at 12:32):

My first question is why does the show command succeed? I assumed that what show X did was that it first checked that X made sense, and then checked that it was defeq to the goal.

I was going to mention this before with your X = Y into X' = Y problem - you could have just written show X' = _. The reason this works is because the checking is done in a weak mode that tolerates metavariable generation, and the second defeq step is not just checking defeq, it is unifying with the target. This means that the first stage will create metavariables and the second stage will unfold stuff as needed to figure out the metavariables. If it can't completely solve the metavariables, you will get new goals instead of an error.

example : tt = tt :=
begin
  show (λ x, tt) _ = tt,
  -- ⊢ (λ (x : ?m_1), tt) ?m_2 = tt
end

example : tt = tt :=
begin
  change (λ x, tt) _ = tt,
  -- ⊢ (λ (x : ?m_1), tt) ?m_2 = tt
  -- ⊢ Sort ?
  -- ⊢ ?m_1
end

As you can see, show differs slightly in that it doesn't change the number of goals while change will add all those unsolved metavariables as new goals, just like refine would.

view this post on Zulip Mario Carneiro (Mar 13 2018 at 12:35):

By the way, goals that look like your phi ⟨A.val + B.val, _⟩ = ⟨B.val + A.val, _⟩ often don't work (they fail in the first stage of parsing), because the anonymous constructor can't be solved outright. In this case it works because phi is sufficient to deduce that both constructors are fin.

view this post on Zulip Mario Carneiro (Mar 13 2018 at 12:48):

My second question is why does rw fail. I have heard rumours that rw will not work inside a lambda (although I don't really understand why -- why is this?) but this is not a lambda and I think the reason for failure is something else.

rw is very sensitive to dependencies. (Or more accurately, it is sufficiently insensitive to dependencies that it will generally fail in their presence.) Both rw and generalize are built on the same basic underlying internal tactic kabstract, which is supposed to take a term P[T] containing a subterm T, and replace it with a variable x. This is needed to construct the motive of the eq.rec application that goes in the proof term when using rw, and it's what you see directly if you use generalize.

The strategy is very simple: look through the term for any subterms that match T (up to some very light unfolding), and replace them with x. It should be obvious that this can get you into trouble when you have dependencies. For example, if two_pos : 0 < 2 then <2, two_pos> is a well typed element of fin 2, but if you simply replace 2 with x you get <x, two_pos> which is not in either fin x or fin 2, it's just malformed. It is actually really difficult to do this correctly in general; in this case you would probably want to generalize the proof of two_pos first so that it will "ride the wave" of 2 -> x renaming rather than being stuck talking about the fixed number 2.

As it pertains to your example, the error message is fairly clear, although it would be more obvious with set_option pp.proofs true. The left argument to the fin constructor has been generalized from A.val + B.val to _a, but the right argument, the proof, is still a proof of A.val + B.val < m + n (namely add_lt_add A.is_lt B.is_lt, what you ended up with after the unfolding), and this is not a correct proof of _a < m + n.

The other major rewrite engine in lean is simp, which does not use kabstract. It operates by using congruence lemmas to recurse into subterms, and this strategy makes it much more reliably type-correct when it comes to rewriting under dependencies. If you try to use simp to rewrite here, it will work, and the proof argument will change to a cast of some sort to accommodate the new type.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 12:48):

Is it possible for me to watch all this unification taking place explicitly? i.e. some set_option?

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 12:51):

[that was about the show / change stuff]

view this post on Zulip Mario Carneiro (Mar 13 2018 at 12:52):

I think set_option trace.type_context.is_def_eq true is what you want

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 12:52):

Earlier on I realised that I didn't really know what rw did, so I've just spent 20 minutes doing edge cases and now I can understand the rw issue. I found that rw doesn't commute with eq.symm in general :-)

view this post on Zulip Sebastian Ullrich (Mar 13 2018 at 12:52):

Plus ...is_def_eq_detail, probably

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 12:54):

example (a b: ℕ) : b + a = b + a + a + b := begin
rw add_comm, -- a + b = a + b + a + b
end

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 12:57):

Are the set_option options documented anywhere?

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:06):

#help options seems to do the trick. (I had to search the code to find that gem. #help is such a rarely used command for me, I'm not even really sure what's there...)

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:39):

I am not even sure if I knew #help existed. I thought the help command in Lean was #print

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:40):

it certainly does seem to be a large overlap of duties

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:40):

I can use conv to rewrite A.val + B.val in that earlier example.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:40):

@[elab_simple] def subtypeadd {m : ℕ} {n : ℕ} (A : fin m) (B : fin n) : fin (m+n) :=
  ⟨A.val+B.val,add_lt_add A.is_lt B.is_lt⟩

definition phi {m n : ℕ} : fin (m + n) → fin (n + m) := λ ⟨i,Hi⟩, ⟨i,add_comm m n ▸ Hi⟩

example {m n : ℕ} (A : fin m) (B : fin n) : phi (subtypeadd A B) = subtypeadd B A :=
begin
  have H : A.val + B.val = B.val + A.val := add_comm _ _,
  -- unfold subtypeadd using show
  show phi ⟨A.val + B.val, _⟩ = ⟨B.val + A.val, _⟩,
  conv
  begin
  congr,
  congr,
  congr,
  rw H,
  end, -- is the term on the left OK??
  admit
end

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:41):

conv is doing all sorts of funny things here

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:41):

It seems to forget some terms

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:41):

and I managed to do a rewrite which earlier on was impossible for a good reason

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:42):

or was it impossible for a bad reason?

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:44):

Oh maybe conv doesn't care about the terms it forgets.

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:44):

I would be in support of moving all "auxiliary" #print stuff to #help; it is a little confusing to have namespace overlapping between #print options (which prints lean cmdline options), #print option (which prints the option type) and #print pp.all (which prints info on the pp.all option)

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:44):

Does conv not bother with subsingletons?

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:44):

I lost a proof

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:46):

I see. So fin is a structure so I can build things of type fin n and they will be of the form <value,proof that this value is less than n>

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:47):

but there's nothing stopping me from deviously changing the value without changing the proof

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:47):

By the way, if you are actually interested in this theorem, a short proof is fin.eq_of_veq (add_comm _ _)

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:49):

I don't need the theorem, I was experimenting with trying to build goals which the prettyprinter wouldn't let me use show with ("show <what the pretty printer says the goal is>" failing)

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:49):

conv uses congrence lemmas, like simp, to traverse the term, certainly if you are using the congr tactic

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:49):

so it will succeed for the same reason that simp does

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:49):

conv is really useful for a learner like me.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:50):

It enables to you really zoom in to parts of complicated things which beginners have trouble manipulating

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:50):

You should turn on pp.proofs while working with this

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:50):

oh that's a cool option

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:51):

lol I remember the days when it was the only option. It's like 80% a good idea to hide proofs

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:51):

is there a command which just changes the state of every option that is available?

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:51):

then I could easily see all the other things I'm missing

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:51):

lol that would be bedlam

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:52):

Imagine how much I'd learn

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:52):

If you care about printing, look at completions for set_option pp.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:53):

I remember getting really confused early on because of those _s in goals which I'd completely forgotten what they stood for

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:53):

It would be even better if it said what they were a proof of

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:53):

That was proposed; but it would make things even harder for the copy-pasters

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:54):

why not make it an option?

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:54):

I don't want to have to edit all those types out

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:54):

to make it compile

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:54):

Oh wooah if I set proofs on, then does "show (goal)" always succeed?

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:54):

no, silly

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:55):

:-)

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:55):

does that solve the halting problem or something?

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:55):

there are a thousand and one edge cases that cause bad printing

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:55):

Oh OK.

view this post on Zulip Mario Carneiro (Mar 13 2018 at 13:55):

even pp.all sometimes fails

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 13:55):

o_O

view this post on Zulip Mario Carneiro (Mar 13 2018 at 14:01):

Here's an example:

theorem T : nat.zero = nat.zero :=
by have f := (λ {x}, eq.refl x); exact f

set_option pp.all true
#print T
theorem T' : @eq.{1} nat nat.zero nat.zero :=
@(λ {x : nat}, @eq.refl.{1} nat x) nat.zero --parse error

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:03):

Oh maybe we're talking at cross purposes.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:03):

theorem T' : @eq.{1} nat nat.zero nat.zero :=
begin
show @eq.{1} nat nat.zero nat.zero -- succeeds
end

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:04):

I was wondering if one could be in tactic mode in a situation where the goal is represented by some string S, and then show S fails

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:07):

I am pretty sure I've done that before, but I am less sure about having done it with pp.all true

view this post on Zulip Mario Carneiro (Mar 13 2018 at 14:16):

It's easiest to demonstrate by using #print to view proof terms, but this affects all printing, and you can make it work with target printing as well by a similar mechanism.

--set_option pp.all true
theorem T : nat.le nat.zero (by have f := (λ {x:ℕ}, 0); exact @f nat.zero) :=
begin
  -- ⊢ nat.le 0 (λ {x : ℕ}, 0)
  change nat.le 0 (λ {x : ℕ}, 0), --fail
  change nat.le nat.zero (@(λ {x : nat}, @has_zero.zero.{0} nat nat.has_zero) nat.zero) -- parse error
end

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:26):

Are these bugs in the prettyprinter? Or just interesting features?

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:27):

Or should @(lam {x},...) actually work?

view this post on Zulip Sebastian Ullrich (Mar 13 2018 at 14:29):

It's the pretty printer wishing for a feature the parser hasn't implemented yet

view this post on Zulip Sebastian Ullrich (Mar 13 2018 at 14:30):

Slightly passive-agressive behavior

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:46):

I see. The pretty printer is somehow the anti-parser isn't it.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 14:47):

in fact it's a one-sided inverse, in a perfect world.

view this post on Zulip Patrick Massot (Mar 13 2018 at 14:47):

See #1900

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 16:24):

I am still unclear about one thing in this thread.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 16:24):

example (a b c N : ℕ) (H1 : a = b) (H2 : a < N) (H3 : b < N) :
 (⟨a,H2⟩:fin N) = ⟨b,H3⟩ :=
begin
-- rw H1 fails
conv begin
  to_lhs,congr, -- goal now | a
  rw H1, -- succeeds
  end,
end

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 16:27):

The first rw fails and my understanding is that it fails because it gives rise to a term which is malformed (copying from Mario's comments above). However it seems to be only as malformed as the term I successfully construct using the conv trick.

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 21:41):

I am still none the wiser about this. One conclusion which I've not yet ruled out is simply that whoever wrote rw could have done better, and made that first rw H1 above succeed, because there is nothing in type theory stopping it from succeeding, as we see from the conv approach. Is the reason that rw H1 fails simply that the rw code just doesn't cover this use case?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 21:45):

I think you are missing that the conv version isn't using just rw, it's using rw + congr, and it is applying congr in the place where dependency matters. Once the goal is | a, there is no longer a dependency to worry about, and rw has no problems.

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:05):

But there is nothing stopping someone from beefing up rw so that it works without using conv? It's just some tactic, right?

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:10):

Initially when I heard that rw couldn't rewrite in certain circumstances I thought that this was because of some theoretical type theory issue which was beyond me, but now I am more inclined to believe that it's just beyond rw.

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:10):

This typechecks:

example (a b c N : ℕ) (H1 : a = b) (H2 : a < N) (H3 : b < N) :
 (⟨a,H2⟩:fin N) = ⟨b,H3⟩ := sorry

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:11):

but if I replace sorry with eq.subst H1 _ then all of a sudden I get a type mismatch in the statement (not the proof) of the example.

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:11):

Yes and no. rw does exactly what we want it to, which is to produce an eq.rec term with a well chosen motive. congr applies an appropriate congruence lemma. There are theoretical limitations on what you can prove using eq.rec, and this is why one wouldn't want to change rw for this

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:12):

I opened an issue on dependent rw a while ago, I think it was closed by "use simp instead"

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:13):

I now know from experience that this is not a satisfactory response

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:13):

The reason I got interested in this use of conv was that I had a situation where simp simplified too much

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:14):

so I had to be super-accurate with my rw

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:14):

conv saved me

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:14):

I mean the simp engine, not necessarily simp on its own

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:14):

How do you use the simp engine??

view this post on Zulip Simon Hudon (Mar 14 2018 at 22:14):

Did it simplify too much even when you called simp only [your rules here]?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:14):

You know that simp has a bazillion options, right?

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:15):

Oh that's a good point Simon, I didn't try this

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:15):

Remember when you discovered that unfold is really simp?

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:15):

Are those bazillion options documented? If not, then no I don't know and I don't know how to find out.

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:15):

other than random looking through changelogs and source code

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:15):

which I find about as pleasant as looking through trash cans

view this post on Zulip Simon Hudon (Mar 14 2018 at 22:16):

That would deserve a good amount of documentation, that's true.

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:16):

simp only [h] {single_pass := tt} is pretty close to rw-like rewriting

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:16):

I did know about simp only from TPIL but somehow it's one of those options which I would never use in practice because my initial reaction when I read TPIL was "whyever would you want to use simp only?"

view this post on Zulip Simon Hudon (Mar 14 2018 at 22:17):

And if you identify the lemmas that cause trouble you can disable it specifically with simp [my_rule, - naughty]

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:17):

and it's only more recently as I have become more experienced that I realise I need it, by which time I have forgotten about it

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:17):

and the simp docs which I PR'ed have explanations of how to find out which lemmas are causing trouble

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:17):

And to identify naughty lemmas you can use set_option trace.simplify.rewrite true

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:17):

yeah, I read that in the docs

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:17):

which I wrote

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:17):

because I cannot manage without docs

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:18):

because I am an old man

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:18):

so no I don't know about the bazillion simp options

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:18):

if you just rattled a few off now I might add them to the docs

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:18):

I am in my late 40s :-)

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:18):

structure simp_config :=
(max_steps : nat           := simp.default_max_steps)
(contextual : bool         := ff)
(lift_eq : bool            := tt)
(canonize_instances : bool := tt)
(canonize_proofs : bool    := ff)
(use_axioms : bool         := tt)
(zeta : bool               := tt)
(beta : bool               := tt)
(eta  : bool               := tt)
(proj : bool               := tt) -- reduce projections
(iota : bool               := tt)
(iota_eqn : bool           := ff) -- reduce using all equation lemmas generated by equation/pattern-matching compiler
(constructor_eq : bool     := tt)
(single_pass : bool        := ff)
(fail_if_unchanged         := tt)
(memoize                   := tt)

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:19):

as you can see, leo is hard at work with those docstrings :)

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:25):

two out of 16 ain't bad, as Meat Loaf once said

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:25):

I am now going to have to rewrite some of my updated simp docs which I was editing as this post arrived.

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:26):

About to be deleted: It is well-known that there are a bazillion simp options, although most are known only to the Lean Inner Circle. Examples which mere mortals know about are those documented in the reference manual and Theorem Proving In Lean.

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:32):

That's not even all of it - there is also the underlying command ext_simplify_core with lots of space for configurability. And dsimp has its own variants on all of this.

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:40):

There are more options somehow:

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:41):

simp tactics in interactive mode have a new configuration parameter (discharger : tactic unit) a tactic for discharging subgoals created by the simplifier. If the tactic fails, the simplifier tries to discharge the subgoal by reducing it to true. Example: simp {discharger := assumption}.

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:41):

from the changelog

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:42):

I can't get this to work though

view this post on Zulip Kevin Buzzard (Mar 14 2018 at 22:47):

OK I added some stuff about simp config options and added it to my PR

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:49):

the dischargeris a tactic unit, so you have to write it in non-interactive mode (or else have tactic open, which is I think what Leo did in that quote). simp {discharger := `[assumption]} should work

view this post on Zulip Mario Carneiro (Mar 14 2018 at 22:50):

but it's not that useful compared to simp *


Last updated: May 12 2021 at 23:13 UTC