Как доказать, что термины языка первого порядка являются обоснованными?

Question

В настоящее время я начал работать над доказательством теорем о логике первого порядка в Coq ( VerifiedMathFoundations ). Я доказал теорему дедукции, но затем застрял с леммой 1 для теоремы корректности. Итак, я компактно сформулировал один элегантный фрагмент леммы и приглашаю сообщество взглянуть на него. Это неполное доказательство правильности условий. Как правильно избавиться от пары «впустить»?

(* PUBLIC DOMAIN *)
Require Export Coq.Vectors.Vector.
Require Export Coq.Lists.List.
Require Import Bool.Bool.
Require Import Logic.FunctionalExtensionality.
Require Import Coq.Program.Wf.

Definition SetVars  := nat.
Definition FuncSymb := nat.
Definition PredSymb := nat.
Record FSV := {
 fs : FuncSymb;
 fsv : nat;
}.
Record PSV := MPSV{
 ps : PredSymb;
 psv : nat;
}.
Inductive Terms : Type :=
| FVC :> SetVars -> Terms
| FSC (f:FSV) : (Vector.t Terms (fsv f)) -> Terms.

Definition rela : forall (x y:Terms), Prop.
Proof.
fix rela 2.
intros x y.
destruct y as [s|f t].
+ exact False.
+ refine (or _ _).
  exact (Vector.In x t).
  simple refine (@Vector.fold_left Terms Prop _ False (fsv f) t).
  intros Q e.
  exact (or Q (rela x e)).
Defined.

Definition snglV {A} (a:A) := Vector.cons A a 0 (Vector.nil A).

Definition wfr : @well_founded Terms rela.
Proof.
clear.
unfold well_founded.
assert (H : forall (n:Terms) (a:Terms), (rela a n) -> Acc rela a).
{ fix iHn 1.
  destruct n.
  + simpl. intros a b; destruct b.
  + simpl. intros a Q. destruct Q as [L|R].
    * admit.  (* smth like apply Acc_intro. intros m Hm. apply (iHn a). exact Hm. *)
    * admit.  (* like in /Arith/Wf_nat.v *)
}
intros a.
simple refine (H _ _ _).
exact (FSC (Build_FSV 0 1) (snglV a)).
simpl.
apply or_introl.
constructor.
Defined.

Также доступно здесь: pastebin .

Обновление : По крайней мере, транзитивность необходима для достоверности. Я также начал доказательство, но не закончил.

Fixpoint Tra (a b c:Terms) (Hc : rela c b) (Hb : rela b a) {struct a}: rela c a.
Proof.
destruct a.
+ simpl in * |- *.
  exact Hb.
+ simpl in * |- *.
  destruct Hb.
  - apply or_intror.
    revert f t H .
    fix RECU 1.
    intros f t H.
    (* ... *)
Admitted.

Answer 1

Вы можете сделать это, определив функцию высоты на Terms и показав, что уменьшение rela подразумевает уменьшение высоты:

Require Export Coq.Vectors.Vector.
Require Export Coq.Lists.List.
Require Import Bool.Bool.
Require Import Logic.FunctionalExtensionality.
Require Import Coq.Program.Wf.

Definition SetVars  := nat.
Definition FuncSymb := nat.
Definition PredSymb := nat.
Record FSV := {
 fs : FuncSymb;
 fsv : nat;
}.
Record PSV := MPSV{
 ps : PredSymb;
 psv : nat;
}.

Unset Elimination Schemes.
Inductive Terms : Type :=
| FVC :> SetVars -> Terms
| FSC (f:FSV) : (Vector.t Terms (fsv f)) -> Terms.
Set Elimination Schemes.

Definition Terms_rect (T : Terms -> Type)
                      (H_FVC : forall sv, T (FVC sv))
                      (H_FSC : forall f v, (forall n, T (Vector.nth v n)) -> T (FSC f v)) :=
  fix loopt (t : Terms) : T t :=
    match t with
    | FVC sv  => H_FVC sv
    | FSC f v =>
      let fix loopv s (v : Vector.t Terms s) : forall n, T (Vector.nth v n) :=
        match v with
        | @Vector.nil _ => Fin.case0 _
        | @Vector.cons _ t _ v => fun n => Fin.caseS' n (fun n => T (Vector.nth (Vector.cons _ t _ v) n))
                                                      (loopt t)
                                                      (loopv _ v)
        end in
      H_FSC f v (loopv _ v)
    end.

Definition Terms_ind := Terms_rect.

Fixpoint height (t : Terms) : nat :=
  match t with
  | FVC _ => 0
  | FSC f v => S (Vector.fold_right (fun t acc => Nat.max acc (height t)) v 0)
  end.

Definition rela : forall (x y:Terms), Prop.
Proof.
fix rela 2.
intros x y.
destruct y as [s|f t].
+ exact False.
+ refine (or _ _).
  exact (Vector.In x t).
  simple refine (@Vector.fold_left Terms Prop _ False (fsv f) t).
  intros Q e.
  exact (or Q (rela x e)).
Defined.

Require Import Lia.

Definition wfr : @well_founded Terms rela.
Proof.
apply (Wf_nat.well_founded_lt_compat _ height).
intros t1 t2. induction t2 as [sv2|f2 v2 IH]; simpl; try easy.
intros [t_v|t_sub]; apply Lt.le_lt_n_Sm.
{ clear IH. induction t_v; simpl; lia. }
revert v2 IH t_sub; generalize (fsv f2); clear f2.
intros k v2 IH t_sub.
enough (H : exists n, rela t1 (Vector.nth v2 n)).
{ destruct H as [n H]. apply IH in H. clear IH t_sub.
  transitivity (height (Vector.nth v2 n)); try lia; clear H.
  induction v2 as [|t2 m v2 IHv2].
  - inversion n.
  - apply (Fin.caseS' n); clear n; simpl; try lia.
    intros n. specialize (IHv2 n). lia. }
clear IH.
assert (H : Vector.fold_right (fun t Q => Q \/ rela t1 t) v2 False).
{ revert t_sub; generalize False.
  induction v2 as [|t2 n v2]; simpl in *; trivial.
  intros P H; specialize (IHv2 _ H); clear H.
  induction v2 as [|t2' n v2 IHv2']; simpl in *; tauto. }
clear t_sub.
induction v2 as [|t2 k v2 IH]; simpl in *; try easy.
destruct H as [H|H].
- apply IH in H.
  destruct H as [n Hn].
  now exists (Fin.FS n).
- now exists Fin.F1.
Qed.

(Обратите внимание на использование пользовательского принципа индукции, который необходим из-за вложенных индуктивов.)

Однако этот стиль разработки слишком сложен. Избежание определенных ловушек значительно упростит это:

1. Стандартная векторная библиотека Coq слишком сложна в использовании. Проблема здесь усугубляется из-за вложенных индуктивных элементов. Вероятно, было бы лучше использовать простые списки и иметь отдельный предикат правильной формы в терминах.

2. Определение отношения, такого как rela в режиме проверки, усложняет чтение. Рассмотрим, например, следующую более простую альтернативу:

   Fixpoint rela x y :=
     match y with
     | FVC _ => False
     | FSC f v =>
       Vector.In x v \/
       Vector.fold_right (fun z P => rela x z \/ P) v False
     end.
   

3. Складывание влево имеет плохое поведение редукции, потому что оно заставляет нас обобщать аргумент накопителя, чтобы пройти через индукцию. Вот почему в моем доказательстве мне пришлось переключиться на fold_right.