Исправить поле с характеристикой, отличной от 2 в Изабель - PullRequest
Новая
       31

Исправить поле с характеристикой, отличной от 2 в Изабель

1 голос
/ 03 ноября 2019

Я сделал доказательство для эллиптических кривых, взяв за основу действительные поля.

Теперь я хочу изменить вещественные числа произвольным полем, характеристика которого отличается от 2, так что из уравнения 2x = 0 можно вывести, что x = 0.

Как получается одна фразаэто в ассистенте доказательства, как Изабель?

1 Ответ

1 голос
/ 03 ноября 2019

По сути, вы можете использовать 

class ell_field = field +
  assumes zero_ne_two: "2 ≠ 0"

Например, см. Сводный закон для эллиптических кривых Штефана Бергхофера .

Я предполагаю, чтоВы хотите работать с классом field из основной библиотеки объектной логики HOL. К сожалению, я не знаю общего подхода к характеристикам кольца в вышеупомянутой библиотеке (надеюсь, если он существует, кто-то укажет нам на это). Поэтому я разработал собственную структуру определения, чтобы дать этому ответу контекст: 

context semiring_1
begin

definition characteristic :: "'a itself ⇒ nat" where
  "characteristic a = 
    (if (∃n. n ≥ 1 ∧ of_nat n = 0) 
    then (LEAST n. n ≥ 1 ∧ of_nat n = 0) 
    else 0)"

end

class ell_field = field +
  assumes zero_ne_two: "2 ≠ 0"
begin

lemma x2: "2 * x = 0 ⟹ x = 0"
  by (simp add: zero_ne_two)

lemma "characteristic TYPE('a) ≠ 2"
proof(rule ccontr, simp)
  assume c2: "characteristic TYPE('a) = 2"
  define P where "P = (λn. (n ≥ 1 ∧ of_nat n = 0))" 
  from c2 have ex: "∃n. P n" 
    unfolding P_def characteristic_def by presburger
  with c2 have least_2: "(LEAST n. P n) = 2"
    unfolding characteristic_def P_def by auto
  from LeastI2_ex[OF ex, of P] have "P (LEAST n. P n)" by simp
  then have "2 = 0" unfolding least_2 unfolding P_def by simp
  with zero_ne_two show False by simp
qed

end
...