Coq Program Fixpoint Obligation Proof

Question

I am trying to write a following program that differentiate an arithmetic formula e with a variable x, called diff with Coq as follows:

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.

I already proved 3 obligations, but 2 are still remaining and I stuck with the rank e < rank (Sum l) where e is an element of l. How can I get the fact that e is from l from the following propositions:

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

Thank you in advance.

Here is the proofs of the obligation that I already proved for who have willing to find the proof:

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

Require Import ZArith String List Program Lia.
Import ListNotations.

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 _ | Var _ | Power _ _  => 0
| Times xs | Sum xs => 1 + list_sum (map rank xs)
end.

Lemma list_sum_cons a l: list_sum (a::l) = a + list_sum l.
Proof. reflexivity. Qed.

Lemma rank_lt (xs:list aexp):
   forall x, In x xs -> rank x < 1 + list_sum (map rank xs).
   induction xs. now inversion 1.
   intros x H; destruct x. 
   1,2,3: now unfold rank; apply Nat.lt_0_succ.
   1,2:destruct H; rewrite map_cons, list_sum_cons; subst.
   2,4: eapply Nat.lt_le_trans; [ apply IHxs, H | ].
   all:lia.
Qed.

Program Fixpoint diff s (x:aexp) {measure (rank x)}: aexp :=
match x with
| Const _ => Const 0
| Var v => Const (if eqb s v then 1 else 0)
| Power v z => 
   if negb (String.eqb v s) then Const 0
   else if Z.eqb z 0 then Const 0
   else if Z.gtb z 0 then Times [Const z; Power v (z - 1)]
   else  Var "ERROR"
| Times xs => Sum (map (fun i => 
        Times ([] 
        ++ (firstn i xs
        ++ [diff s (nth i xs (Const 0))]
        ++ skipn (1+i) xs)))
       (seq 0 (length xs)))
| Sum xs => Sum (map (fun i => diff s (nth i xs (Const 0))) (seq 0 (length xs)))
end.

Next Obligation.
destruct (lt_dec i (length xs)) as [H|H].
- apply (rank_lt _ _ (nth_In _ _ H)).
- rewrite nth_overflow. 
   apply Nat.lt_0_succ. 
   lia.
Defined.

Answer 2

I am allowing empty sums and prods (the former should evaluate to 0, the latter to 1), so recursion on lists of aexp can be done uniformly and with no exceptions.

I'd also extend aexpr with a NaN, to use in place of the Var "ERROR", which then compels handling all cases including the "exceptional" ones correctly, while you are in fact not doing that at the moment. -- But I'll leave this as an exercise for you.

Last but not least, (regardless of specific conventions and styles) a bit cleaner, more uniform, and more explicit code also helps readability a lot.

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

Import ListNotations.

Inductive aexp : Set :=
| Con (n : Z)
| Var (s : string)
| Pow (s : string) (n : Z)
| 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 0 else 1)
  | (* D_s a**n := (n >= 0) ->
        n = 0 || a <> s ? 0 : n*(a**(n-1)) *)
    Pow a n =>
      if Z.ltb n 0 then Var "ERROR"
      else if Z.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.
Next Obligation.
  destruct x'.
  all: cbn; lia.
Defined.