Какова противоположная (?) Команда "econstructor"

Question

Например,

Lemma ex_1:
exists n, n=1.
Proof.

показывает одну подцель:

exists n : nat, n = 1

команда econstructor меняет цель на

?n = 1

, какая команда можетполучить

exists n : nat, n = 1

снова из "? n = 1"?

или, скажем, мы доказали некоторую подзадачу с (существует n, ~) формой для этого.Как мы можем «применить» сублемму?

Answer 1

Тео Винтерхальтер дал несколько стратегий, которые работают в этом случае, но в целом, econstructor необратим в нескольких смыслах.

econstructor может привести два разных состояния доказательства к одному и тому же конечному состоянию.

То есть econstructor не является инъективным в отношении состояний доказательства.Например, рассмотрим эту (довольно глупую) ситуацию.

Inductive exists': Prop :=
| intro (n: nat): n = 1 -> exists'.

Goal exists'.
Proof.
  econstructor.

В итоге мы получим одно и то же конечное состояние, даже если начальная цель (до econstructor) была другой.

econstructor в целом теряет информацию.

Даже если мы знаем, каково было первоначальное состояние, возврат к нему может быть невозможен.В этом примере мы будем использовать inhabited из стандартной библиотеки, но она работает так же хорошо для exists, поскольку inhabited A эквивалентно exists a: A, True.

Goal forall A: Type, inhabited A -> inhabited A.
Proof.
  intros A H.
  econstructor.

Теперь доказательствосостояние

1 subgoal
A : Type
H : inhabited A
______________________________________(1/1)
A

, и мы хотели бы использовать H для решения цели.Но это (в общем) невозможно.Мы не можем начать с простого утверждения, что элемент типа A существует, и сгенерировать фактический термин типа A.Проблема в том, что, поскольку H является Prop, мы можем уничтожить его (или сопоставить с ним), если цель также равна Prop.После использования econstructor это уже не так, поэтому у нас должен быть явный свидетель типа A.В вашем примере это работает, поскольку мы точно знаем, какой элемент nat удовлетворяет n = 1, но в целом мы не можем знать, что

Помощник по доказательствам Lean использует общеговыражение forall A, nonempty A -> A (nonempty совпадает с inhabited Coq) для питания его классической логической библиотеки.То же самое доказательство исключенных промежуточных работ в Coq (при условии функциональной экстенсиональности и экспозиционной экстенсиональности).Итак, если у нас есть forall A: Type, inhabited A -> A, то закон исключенной средней и даже некоторые сильные версии аксиомы выбора доказуемы (с добавлением некоторых аксиом экстенсиональности).

---

Также обратите вниманиечто при использовании econstructor любые экзистенциальные переменные должны в конечном итоге создаваться со значениями, существующими в контексте current .Если у вас H: exists n: nat, n = 1, вам придется уничтожить H до , используя econstructor.

Hypothesis H: exists n: nat, n = 1.

Goal exists n: nat, n = 1.
Proof.
  destruct H as [x H].
  econstructor.
  exact H.
Defined.

Goal exists n: nat, n = 1.
Proof.
  econstructor.
  destruct H as [x H].
  Fail exact H.
Abort.

Answer 2

Если у вас есть гипотеза

H : exists n : nat, n = 1

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

destruct H as [n Hn]

чтобы получить гипотезу

n : nat
Hn : n = 1

Вот как вы используете такую ​​информацию.

Что касается другой части вопроса, мне нужно будет увидеть пример того, что вы пытаетесь сделать. Здесь вы используете econstructor (это также может быть eexists), так что вы получите экзистенциальную переменную ?n в вашем контексте, и тогда она будет решена с помощью unification . Например, вы затем решаете ?n = 1 по reflexivity, что является доказательством 1 = 1, поэтому Кок знает, что ?n должно быть 1.

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

exists 1. reflexivity.