induction tactic failed

Stream: new members

[Alex Zhang]

This is an #mwe I extracted, how can I get across this problem?

import tactic
import field_theory.finite.basic
import number_theory.quadratic_reciprocity

variables {F : Type*} [field F] [fintype F] [decidable_eq F]
example : field F :=
begin
  have exist_p := char_p.exists F,
  cases exist_p,
end

[Alex Zhang]

the error message is induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop

[Reid Barton]

This example is too minimal

[Reid Barton]

obviously, you should just use the [field F] hypothesis here

[Reid Barton]

The error message means: you can't do cases on an existential when you're trying to define data (like a field instance)

[Reid Barton]

In this case though, a field has exactly one characteristic. So there must be something other than char_p.exists you can use to get it.

[Alex Zhang]

The key problem is how I can extract a char for F in a definition constructing something.
The thing can even be a graph

import tactic
import field_theory.finite.basic
import combinatorics.simple_graph.basic

variables {F V : Type*} [field F] [fintype F] [decidable_eq F]

include F
example : simple_graph V :=
begin
  have exist_p := char_p.exists F,
    cases exist_p,
end

[Alex Zhang]

cases or rcases or obtain will report errors

[Reid Barton]

char_p.exists is the wrong thing to use here.

[Reid Barton]

What you want is the characteristic of the field, not just knowing that it has some characteristic.

[Alex Zhang]

What should be the right lemma to use then? :thinking:

[Reid Barton]

You don't want a lemma, you want a definition.

[Reid Barton]

I would just read random files about fields until I found out what it is.

[Alex Zhang]

Yeah, I want a def based on the char of F.

[Reid Barton]

Also, it's usually not a good idea to make a definition using tactics unless you're careful about which tactics you use where.

[Reid Barton]

Because later you're presumably going to want to prove something about what you defined, and for that you will need to know what term was produced (and you probably don't want that term to start with something like have exist_p := char_p.exists F, exist_p.rec (\lam p, ...))

[Adam Topaz]

You can use docs#ring_char to get the characteristic of a field (or even a possibly non associative semiring) as a natural number. I would also take a look at how it's implemented which should help with some of the questions you have above.

[Adam Topaz]

The associated API should all have the form ring_char.foo

[Eric Rodriguez]

in general, though, if you have a goal with typing judgement in Type* and you want to get the data out of an Exists, then you have to use classical.some and classical.some_spec; I've suggested a obtain! that lets you get round this error, but I haven't gotten round to coding it. The reason that you can even obtain on ∃ when you're making a Prop is because of proof irrelevance

[Kevin Buzzard]

It's also worth remarking that if you have a tactic mode goal whose type is Type* then you're probably doing something wrong anyway: goals should have type Prop in tactic mode.

[Alex Zhang]

If it is to construct an instance of some class containing only several propositions, I don't see a problem with using tactics.

[Kevin Buzzard]

simple_graph contains adj, which is data.

[Kevin Buzzard]

If a class just contains propositions, then it will be a proposition itself.

[Kevin Buzzard]

To make an instance of any structure (e.g. a class) I guess the standard way to do it is to use the usual constructor, e.g.

example : simple_graph V :=
{ adj := _,
  sym := _,
  loopless := _ }

rather than launching into tactic mode with begin.

[Alex Zhang]

Yeah, simple_graph is not an example for a class of props.

[Alex Zhang]

nontrivial is an example

[Kevin Buzzard]

right, and it's a Prop, so you can use begin/end for that, but it would probably be wiser to use some structure constructor instead for example ⟨begin ... end⟩

[Reid Barton]

Alex Zhang said:

nontrivial is an example

Right but you wouldn't have gotten the original error about Exists.dcases_on if your goal was really a Prop. That's why I suggested the example was too minimized.

[Alex Zhang]

Ah, I see, if the type of the structure is :Prop , the problem will not occur.

[Kevin Buzzard]

Exactly. cases and other related commands call the recursor for the structure in question, and if the structure only eliminates into Prop then you won't be able to use it in tactic mode if the goal isn't a Prop.

[Alex Zhang]

I encountered this issue as I did not write : Prop is the structure declaration like the following:

import tactic
import field_theory.finite.basic
import number_theory.quadratic_reciprocity

variables {F : Type*} [field F] [fintype F] [decidable_eq F]

class struct1 :=
(prop1 : true)
(prop2 : true)

include F
example : struct1 :=
begin
  have exist_p := char_p.exists F,
  cases exist_p,
end

[Kevin Buzzard]

For example or.rec is

or.rec : ∀ {a b C : Prop}, (a → C) → (b → C) → a ∨ b → C

and because C : Prop you won't be able to do cases on h : a ∨ b if your goal is not a Prop.

[Reid Barton]

Yes, this structure/class defaulting to Type mistake is really easy to make.

[Kevin Buzzard]

One could argue that this is a bug in Lean. This sort of thing even makes its way into mathlib occasionally.

[Eric Rodriguez]

technical sidenote but shouldn't singleton elimination kick in for struct1? or do I understand singleton elimination wrong

[Kevin Buzzard]

exists eliminates into Prop and this has nothing to do with subsingleton elimination. Lean cannot solve for C and that's the end of it, so the cases tactic doesn't work.

[Kevin Buzzard]

As has already been observed, there are other ways around this, but they use other tactics.

[Alex Zhang]

@Eric Rodriguez Could you show how to use classical.some or classical.some_spec in the very first example?

[Eric Rodriguez]

import tactic
import field_theory.finite.basic
import number_theory.quadratic_reciprocity

variables {F : Type*} [field F] [fintype F] [decidable_eq F]
example : field F :=
begin
  have exist_p := char_p.exists F,
  have hp := classical.some_spec exist_p,
  -- hp: char_p F (classical.some exist_p)
end