如何证明这两种类型之间的等价性 - 算法'和算法''？

Question

我在这里做错了什么（要么我太缺乏经验而无法完成证明，要么之前有一些错误）？我不能完全证明这两种类型之间的等价性。任何帮助表示赞赏。

这是我努力证明 log_2(n!) 的排序界限（对于特定的 n=8）的一部分。 algorithm'' 类型对应决策树。

Require Import List Lia.
Set Implicit Arguments.

Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
Inductive variable := aux | num: value -> variable.
Definition variable_eq_dec (x y: variable): {x=y} + {x<>y}.
Proof.
  destruct x, y.
  + left; auto.
  + right; abstract congruence.
  + right; abstract congruence.
  + destruct v, v0; try (left; abstract congruence); (right; abstract congruence).
Defined.

Inductive assignment := assign: variable -> variable -> assignment.
Inductive comparison := GT: forall (more less: value), comparison.

Definition instantation := variable -> nat.

Definition run_assignment (a: assignment) (i: instantation): instantation :=
  match a with
  | assign v1 v2 => fun x => if variable_eq_dec x v1 then i v2 else i x end.

Fixpoint run_assignment_list (L: list assignment): instantation -> instantation :=
  match L with
  | nil => fun i => i
  | a :: l => fun i => run_assignment_list l (run_assignment a i)
  end.

Inductive algorithm': nat -> Type :=
| leaf': algorithm' 0
| conditional': forall n (c: comparison) (pos_assignments neg_assignments: list assignment) (pos neg: algorithm' n), algorithm' (S n).

Inductive algorithm'': nat -> Type :=
| leaf'': list assignment -> algorithm'' 0
| conditional'': forall n (c: comparison) (pos neg: algorithm'' n), algorithm'' (S n).

Definition run_algorithm' n (a: algorithm' n): instantation -> instantation.
Proof.
  induction a.
  + exact (fun x => x).
  + intro i. destruct c. exact (if Compare_dec.gt_dec (i (num more)) (i (num less))
                       then IHa1 (run_assignment_list pos_assignments i)
                       else IHa2 (run_assignment_list neg_assignments i)).
Defined.

Definition run_algorithm'' n (a: algorithm'' n) (i: instantation): instantation.
Proof.
  induction a.
  + exact (run_assignment_list l i).
  + destruct c.
    exact (if Compare_dec.gt_dec (i (num more)) (i (num less)) then IHa1 else IHa2).
Defined.

Fixpoint append_assignments n (a: algorithm'' n) (L: list assignment): algorithm'' n :=
  match a with
  | leaf'' L0 => leaf'' (L ++ L0)
  | conditional'' c pos neg => conditional'' c (append_assignments pos L) (append_assignments neg L)
  end.

Fixpoint algorithm'_to_algorithm'' n (a: algorithm' n): algorithm'' n :=
  match a with
  | leaf' => leaf'' nil
  | conditional' c Lpos Lneg pos neg =>
      conditional'' c (append_assignments (algorithm'_to_algorithm'' pos) Lpos)
                      (append_assignments (algorithm'_to_algorithm'' neg) Lneg)
  end.

Theorem algorithm'_algorithm''_equiv n (a: algorithm' n):
  forall (i: instantation) (x: variable), run_algorithm' a i x = run_algorithm'' (algorithm'_to_algorithm'' a) i x.
Proof.
Admitted.

Answer 1

您的陈述似乎是错误的。这是一个反例。

Definition mya1 : algorithm' 2 := 
  conditional' (GT x0 x1)
     ((assign (num x0) (num x2)) :: (assign (num x1) (num x3)) :: nil)
     ((assign (num x0) (num x4)) :: (assign (num x1) (num x5)) :: nil)
   (conditional' (GT x2 x3)
     ((assign (num x2) (num x6)) :: (assign (num x3) (num x7)) :: nil)
     ((assign (num x0) (num x4)) :: (assign (num x1) (num x5)) :: nil)
     leaf' leaf')
   (conditional' (GT x3 x0)
     ((assign (num x2) (num x7)) :: (assign (num x3) (num x6)) :: nil)
     ((assign (num x0) (num x4)) :: (assign (num x1) (num x5)) :: nil)
     leaf' leaf').

Definition myi x := 
         if variable_eq_dec x (num x0) then 3 else 
         if variable_eq_dec x (num x1) then 4 else 
         if variable_eq_dec x (num x2) then 6 else
         if variable_eq_dec x (num x3) then 5 else 
         if variable_eq_dec x (num x4) then 7 else 
         if variable_eq_dec x (num x5) then 8 else 
         if variable_eq_dec x (num x6) then 9 else 
         0.

以下命令返回6

 Compute run_algorithm' mya1 myi (num x2).

虽然以下返回0。

 Compute run_algorithm'' (algorithm'_to_algorithm'' mya1) myi (num x2).

我通过尝试对a 进行归纳证明找到了反例。这是我的脚本。

Theorem algorithm'_algorithm''_equiv n (a: algorithm' n):
  forall (i: instantation) (x: variable), 
 run_algorithm' a i x  = run_algorithm'' (algorithm'_to_algorithm'' a) i x.
Proof.
induction a.
  easy.
simpl.
intros i x.
destruct c.
destruct (Compare_dec.gt_dec (i (num more)) (i (num less))) as [cmp1 | cmp2].
  rewrite IHa1.

这让我有了一个更多关于append_assigments 和run_assignment_list 的目标，我以这种方式陈述。

Lemma algorithm''_list n (a : algorithm'' n) (l: list assignment) i x :
  run_algorithm'' a (run_assignment_list l i) x =
  run_algorithm'' (append_assignments a l) i x.

在做这个证明的过程中，通过对a 的归纳，我可以看到等式两边的执行不匹配。进一步分析得出反例。