declare unique constants

Stream: new members

[Quinn Culver]

Is there a way to declare unique constant terms ? My ideas:

1. First do constants a b c d : nat, then declare an axiom stipulating them pairwise distinct. That feels like too much work for this.
2. Declare (a b c d) to be a set; so something like constant (a b c d) : set nat, but that doesn't work and I can't find any syntax to make it work.

[Junyan Xu]

You may want to use docs#list.nodup like [a, b, c, d].nodup.

[Quinn Culver]

Thanks. I did

constants a b c d : ℕ
axiom distincts : [a, b, c, d].nodup
#eval a==b

Why doesn't the last line work to verify that it worked? How can I verify it?

[Mario Carneiro]

one way is

example : a ≠ b := λ h, by simpa [h, list.nodup] using distincts

[Mario Carneiro]

you can't evaluate a = b using #eval because a and b don't have values that are accessible to the compiler (they are "noncomputable")

[Junyan Xu]

A general way to get out the individual inequalities:

import data.list.nodup

constant α : Type*
constants a b c d : α
axiom distinct : [a,b,c,d].nodup

example : a ≠ b := list.pairwise_iff_nth_le.1 distinct 0 1 dec_trivial dec_trivial

(replace 0 and 1 by indices of the elements)

[Junyan Xu]

Maybe we should have a lemma like docs#list.tfae.out for docs#list.pairwise

[Patrick Johnson]

Introducing an axiom is a bad idea. You should use choice instead.

import tactic
import tactic.induction

noncomputable theory
open_locale classical

lemma aux {l : list ℕ} {i : ℕ} {hh} : l.nth_le i hh ≤ l.sum :=
begin
  induction' l with x l ih,
  { cases hh },
  { rw [list.nth_le_cons, list.sum_cons], cases i,
    { simp },
    { rw dif_neg, swap, { simp },
      simp only [nat.succ_sub_succ_eq_sub, tsub_zero],
      transitivity l.sum,
      { apply ih },
      { exact le_add_self }}},
end

lemma exi (n : ℕ) : ∃ (l : list ℕ), l.length = n ∧ l.nodup :=
begin
  induction n with n ih,
  { use [[]], simp },
  { rcases ih with ⟨l, h₁, h₂⟩, use [l.sum.succ :: l, by simp [h₁]],
    rw [list.nodup_cons, list.mem_iff_nth_le], refine ⟨_, h₂⟩,
    push_neg, rintro i h₃, apply ne_of_lt, rw nat.lt_succ_iff, exact aux },
end

def abcd := (exi 4).some

[Quinn Culver]

Thanks @Patrick Johnson . Mind explaining your method in higher-level language ?

[Quinn Culver]

Once I have those four unique constants, which---possibly relevantly---aren't actually natural numbers, I want to declare an axiom stating something about all subsets of {a,b,c,d} with cardinality 3. Must/should I declare a finset for that? If so, how to do that? I gather from the docs that I need to provide a multiset and a proof of finiteness, but I'm unclear about the syntax for multisets and how to prove finiteness. FWIW, I'd rather not be given explicit solutions; I'd prefer hints or similar examples.

[Kevin Buzzard]

You don't want to declare an axiom, you want to assume a hypothesis. No you don't have to use finsets. There are four ways to do finiteness in Lean and probably all of them can be made to work. Don't make a finset from a multiset, just because that's how finsets are constructed under the hood doesn't mean that that's how you need to construct them. As for hints instead of solutions, why not instead ask for solutions to explicit easier questions? Post a #mwe .

[Eric Wieser]

If you're not actually asking for them to be natural numbers, it sounds to me like you might want

@[derive [fintype, decidable_eq]]
inductive my_type
| a
| b
| c
| d

This gives you the 4 elements and the fact they are distinct axiomatically, but in a much more sound way than with axiom.

[Eric Wieser]

You can then get the sets with cardinality 3 as (finset.univ : finset my_type).powerset_len 3

[Eric Wieser]

(docs#finset.powerset_len)

[Junyan Xu]

From this topic I think @Quinn Culver cares about something like four distinct points on the plane / in a space? Then maybe instead of declaring four constants you should use a finset X of docs#finset.card equal to 4, where X is the space; maybe the space should be a structure with X the type of points together with some axioms as its fields.

[Yaël Dillies]

Let me also mention docs#finset.card_eq_three

[Quinn Culver]

@Junyan Xu is right. I'm formalizing the axioms for a projective plane, the third of which says that there are four (distinct) points no three of which are colinear. Thanks for the suggestion @Kevin Buzzard, I'll follow that in the future.

[Quinn Culver]

@Junyan Xu , once I declare a finset with constant A : finset Point, do I need to declare its cardinality separately? As an axiom? Like this: axiom A_card_is_four : finset.card A = 4?

[Quinn Culver]

@Kevin Buzzard I don't understand your statement "You don't want to declare an axiom, you want to assume a hypothesis." Do you still think that even though I'm trying to formalize the projective plane axiom stating that there are four (distinct) points no three of which are colinear?

[Ruben Van de Velde]

Yeah, you probably want to write theorems assuming "P is a projective plane"

[Quinn Culver]

Wow, I just noticed that projective planes are in mathlib! :embarrassed:

[Patrick Johnson]

Whatever you're formalizing, you certainly don't want to use keyword axiom. What you actually want is structure. See docs#configuration.projective_plane for example.

[Quinn Culver]

Good to know. I'm a little confused then about when it is appropriate to use axiom.

[Alex J. Best]

On paper we use the word axiom a lot more flexibly than the lean keyword axiom. For example we often say that $1 * g = g$ is an axiom of a group. But axioms in lean are reserved mostly for things that you need to start setting up the foundations of mathematics, more like the axioms of zfc set theory that underlie all different types of mathematics. You can add new lean axioms if you want, but most users never need to and never do.

[Junyan Xu]

There are three built-in axioms in Lean, and if you want to contribute to mathlib, I don't think you're allowed to add any axiom in your code.

[Patrick Massot]

The word axiom already has a different meaning when you say "axiom of a group" and "axiom of Zermelo Frankel", this has nothing specific to formalized mathematics.

[Quinn Culver]

@Patrick Massot Mind elaborating on the difference b/t "axiom of a group" and "axiom of ZF"?

[Kevin Buzzard]

The axioms of ZF are fixed before you start and never go away. The "axioms" of a group are just transient hypotheses.

[Martin Dvořák]

Unpopular opinion: I sometimes use axiom to check stuff like "this lemma is the only thing missing to have my big theorem verified".

[Eric Wieser]

sorry is reasonably effective for that too; but yes, you can use axiom instead of sorry to precisely track which sorries you still need, since sorry does not give you an error like "this lemma uses foo, bar, baz which contain sorry"

[Eric Wieser]

Although I suspect there is a tactic that produces precisely that message somewhere on Zulip

[Martin Dvořák]

Example:

#check        nnyCF_of_CF_i_CF
#print axioms nnyCF_of_CF_i_CF

After it compiles, the output is:

nnyCF_of_CF_i_CF : ¬∀ (T : Type) (L₁ L₂ : language T), is_CF L₁ ∧ is_CF L₂ → is_CF (L₁ ⊓ L₂)

quot.sound
propext
classical.choice
CF_pumping

This tells me that the proof of [The class of context-free languages is not closed under intersection.] is finished up to the Context-free pumping lemma. If there was an actual sorry anywhere in the "call stack", it would be listed as [sorry] among the axioms.

[Patrick Massot]

Martin, you can use #16911. It isn't merged yet but this is an autonomous single file that you can simply dump into your project until it is merged into mathlib.

[Quinn Culver]

@Kevin Buzzard Might a Platonist disagree by saying both structures are on equal footing and their axioms equally fixed?

[Kevin Buzzard]

The difference is that we are working in ZFC

[Kevin Buzzard]

The structures are most definitely not on the same footing -- things are going on on two different levels

[Kevin Buzzard]

To give an example: you can make a structure that has contradictory axioms and this isn't a problem at all, you just can't make any instances of the structure. But if you add an axiom to your theory making it inconsistent (which you can do with axiom) then this is a huge problem because now you can prove everything.