Проблема с простым утверждением в FStar

Question

Я только начал изучать FStar. Хочу отметить тот факт, что для каждого натурального числа существует большее число.

let _ = assert (forall (m:nat). exists (n: nat). n > m)

Это не удается, и я хотел бы знать, почему. Спасибо.

Answer 1

Количественные формулы, подобные приведенной здесь, по умолчанию обрабатываются с использованием эвристики Z3 для количественной реализации на основе шаблонов. Вы можете узнать больше о шаблонах Z3 здесь: https://rise4fun.com/Z3/tutorialcontent/guide и https://github.com/FStarLang/FStar/wiki/Quantifiers-and-patterns

Короче говоря, вам нужно помочь F* и Z3 найти свидетеля экзистенциального квантора. Один из способов сделать это так:

let lem (m:nat)
  : Lemma (exists (n:nat). n > m)
  = assert (m + 1 > m)

что доказывает лемму, что для любого m:nat существует n:nat лучше чем m. Его доказательство F*+Z3 намекает, чтоm + 1 хороший свидетель для выбора n.

Вы можете превратить подобную лемму в количественное утверждение разными способами. См. FStar.Classical для некоторых примеров этого. Например, это работает:

let _ =
  FStar.Classical.forall_intro lem;
  assert (forall (m:nat). exists (n: nat). n > m)

Вот еще один подход, который позволяет избежать определения промежуточной леммы, но вместо этого использует промежуточное утверждение.

let _ =
  assert (forall (m:nat). m + 1 > m);
  assert (forall (m:nat). exists (n: nat). n > m)