Coq 程序定点义务证明

Question

我正在尝试编写一个以下程序，用 Coq 区分算术公式

e

和变量

x

，称为

diff

，如下：

Inductive aexp : Type :=
| Const : Z -> aexp
| Var : string -> aexp
| Power : string -> Z -> aexp
| Times : list aexp -> aexp
| Sum : list aexp -> aexp.

Fixpoint rank (e:aexp) : nat :=
    match e with
    | Const n => 1
    | Var a => 1
    | Power a n => 1
    | Times l => 1 + (fix sum_rank l :=
                        match l with
                        | [] => 0
                        | hd :: tl => (rank hd) + (sum_rank tl)
                        end) l
    | Sum l => 1 + (fix sum_rank l :=
                        match l with
                        | [] => 0
                        | hd :: tl => (rank hd) + (sum_rank tl)
                        end) l
    end.

Program Fixpoint diff (e:aexp) (x:string) {measure (rank e)} : aexp :=
    match e with
    | Const n => Const 0
    | Var a => (if negb (String.eqb a x) then Const 0 else Const 1)
    | Power a n => (if Z.ltb n  0 then Var "ERROR"
                    else if (Z.eqb n  0) || negb (String.eqb a x) then Const 0
                    else Times [Const n; (Power a (n-1))])
    | Times l => (match l with
                | [] => Var "ERROR"
                | [hd] => diff hd x
                | hd ::tl => Sum [Times ((diff hd x)::tl); Times [hd; diff (Times tl) x]]
    end)
    |Sum l => (match l with
            | [] => Var "ERROR"
            (* | _ => Sum (map (fun e => diff e x) l x) *)
            | _ => Sum (map (fun e => diff e x) l)
            end)
    end.

我已经证明了 3 个义务，但还剩下 2 个义务，我坚持使用

rank e < rank (Sum l)

，其中

e

是

l

的元素。 我怎样才能从以下命题中得到

e

来自

l

的事实：

x : string
l : list aexp
diff : forall e : aexp, string -> rank e < rank (Sum l) -> aexp
n : [] <> l
e : aexp

提前谢谢您。

以下是我已经证明给愿意寻找证据的人的义务证明：

Next Obligation.
Proof.
    simpl.
    rewrite Nat.add_0_r.
    apply Nat.lt_succ_diag_r.
    Qed.
Next Obligation.
Proof.
    simpl.
    rewrite <- Nat.add_succ_r .
    Search (_ < _ + _).    
    rewrite <- Nat.add_0_r at 1.
    rewrite <- Nat.add_lt_mono_l with (p := rank hd).
    assert (forall n, 0 < S n).
    {
        induction n0.
        firstorder.
        firstorder.
    }
    apply H.
Qed.
Next Obligation.
Proof.
    simpl.
    assert (forall e, rank e > 0).
    {
        induction e.
        simpl.
        firstorder.
        simpl.
        firstorder.
        simpl.
        firstorder.
        simpl.
        assert (forall n, 0 < S n).
        {
            induction n0.
            firstorder.
            firstorder.
        }
        apply H.
        simpl.
        assert (forall n, 0 < S n).
        {
            induction n0.
            firstorder.
            firstorder.
        }
        apply H.
    }
    rewrite <- Nat.add_succ_r.
    Search ( _ + _  = _ + _).
    rewrite Nat.add_comm.
    rewrite <- Nat.add_0_r at 1.
    rewrite <- Nat.add_lt_mono_l.
    apply H.
    Qed.

Answer 1

面对这段代码，因为我必须更改一些内容才能了解其本质，其中一些必然是为了可读性，特别是：

• 使用

  nat

  而不是

  Z

  （因为你可以：让事情变得更容易）：当然可以索引变量，并且对于实际上仅意味着非负的指数；
• 允许空和和prods（前者应计算为0，后者应计算为1），因此可以统一进行递归，并且没有例外；
• （无论具体约定和风格如何）更干净、更明确的代码对可读性有很大帮助。

From Coq Require Import String.
From Coq Require Import List.
From Coq Require Import Bool.
From Coq Require Import Lia.
From Coq Require Import Program.

Import ListNotations.

Inductive aexp : Set :=
| Con (n : nat)
| Var (s : string)
| Pow (s : string) (n : nat)
| Sum (xs : list aexp)
| Mul (xs : list aexp).

Fixpoint rank (x : aexp) : nat :=
  match x with
  | Con _
  | Var _
  | Pow _ _ => 1
  | Sum xs
  | Mul xs  => 1 +
      (fix ranks xs :=
        match xs with
        | []        => 0
        | x' :: xs' =>
            rank x' + ranks xs'
        end
      ) xs
  end.

Program Fixpoint diff s x {measure (rank x)} : aexp :=
  match x with
  | (* D_s n := 0 *)
    Con _ => Con 0
  | (* D_s a := a <> s ? 0 : 1 *)
    Var a =>
      Con (if negb (String.eqb a s) then 1 else 0)
  | (* D_s a**n :=
        n = 0 || a <> s ? 0 : n*(a**(n-1)) *)
    Pow a n =>
      if Nat.eqb n 0 ||
        negb (String.eqb a s) then Con 0
      else Mul [Con n; Pow a (n - 1)]
  | (* D_s Sum_i xi :=
        D_s x0 + D_s Sum_{i>0} xi *)
    Sum xs =>
      match xs with
      | []        => Con 0
      | x' :: xs' =>
          Sum [diff s x'; diff s (Sum xs')]
      end
  | (* D_s Mul_i xi :=
        D_s x0 * Mul_{i>0} xi +
        x0 * D_s Mul_{i>0} xi *)
    Mul xs =>
      match xs with
      | [] => Con 0
      | x' :: xs' =>
          Sum [
            Mul [diff s x'; Mul xs'];
            Mul [x'; diff s (Mul xs')]
          ]
      end
  end.
Next Obligation.
  cbn; lia.
Defined.
Next Obligation.
  destruct x'.
  all: cbn; lia.
Defined.
Next Obligation.
  destruct x'.
  all: cbn; lia.
Defined.