Как доказать основные факты о типах данных и кодовых типах?

Я хотел бы доказать некоторые основные факты о datatype_new и codatatype: у первого нет бесконечного элемента, а у второго он есть.

theory Co 
imports BNF 

begin 

datatype_new natural = Zero | Successor natural   

lemma "¬ (∃ x. x = Successor x)" 
oops 

codatatype conat = CoZero | CoSucc conat 

lemma "∃ x. x = CoSucc x" 
oops

Проблема заключалась в том, что я не мог придумать доказательство на бумаге, не говоря уже о сценарии.

Идея первого состояла в том, чтобы использовать функцию размера, которая имеет теорему

size (Successor ?natural) = size ?natural + Suc 0

и каким-то образом, используя это size, это функция, применяя ее к двум частям исходного уравнения, нельзя получить натуральное число, равное его преемнику. Но я не вижу, как я мог бы формализовать это.

Для последнего у меня даже не было идеи, как вывести эту теорему из фактов, которые доказывает пакет codatatype.

Как я могу доказать это?


isabelle
person Gergely    schedule 12.07.2014    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Лично я ничего не знаю о кодовых типах. Но позвольте мне все же попытаться вам помочь.

Первая опубликованная вами лемма может быть автоматически доказана sledgehammer. Он находит доказательство с помощью функции size, эффективно сводя задачу на natural к той же проблеме на nat:

by (metis Scratch.natural.size(2) n_not_Suc_n nat.size(4) size_nat)

Если вам нужна очень простая пошаговая версия этого доказательства, вы можете написать ее так:

lemma "¬(∃x. x = Successor x)" 
proof clarify
  fix x assume "x = Successor x"
  hence "size x = size (Successor x)" by (rule subst) (rule refl)
  also have "... = size x + Suc 0" by (rule natural.size)
  finally have "0 = Suc 0"  by (subst (asm) add_0_iff) (rule sym)
  moreover have "0 ≠ Suc 0" by (rule nat.distinct(1))
  ultimately show False by contradiction
qed

Если вам нужно более «элементарное» доказательство без использования натуральных чисел HOL, вы можете провести доказательство от противного, используя индукцию по вашему natural:

lemma "¬(∃x. x = Successor x)" 
proof clarify
  fix x assume "x = Successor x"
  thus False by (induction x) simp_all
qed

Вы в основном получаете два случая в индукции:

  1. Zero = Successor Zero ⟹ False
  2. ⋀x. (x = Successor x ⟹ False) ⟹ Successor x = Successor (Successor x) ⟹ False

Первая подцель является прямым следствием natural.distinct(1), вторая может быть сведена к гипотезе индукции с помощью natural.inject. Так как эти правила находятся в симпсете, simp_all может решить его автоматически.

Что касается второй леммы, единственное решение, которое я могу придумать, — это явно построить бесконечный элемент, используя primcorec:

primcorec infinity :: conat where
  "infinity = CoSucc infinity"

Затем вы можете доказать свою вторую лемму, просто развернув определение:

lemma "∃x. x = CoSucc x" 
proof
  show "infinity = CoSucc infinity" by (rule infinity.ctr)
qed

Предупреждение: эти доказательства работают, но я не уверен, являются ли они самым простым и/или самым элегантным решением этой проблемы. Я практически ничего не знаю о типах кодовых данных или новом пакете типов данных.

person Manuel Eberl    schedule 12.07.2014