# Implicit Differentiation in Coq — No Reals, No Limits, Just Proof

**URL:** <https://discourse.rocq-prover.org/t/implicit-differentiation-in-coq-no-reals-no-limits-just-proof/2689>\
**Category:** Miscellaneous\
**Created:** [May 6, 2025, 3:08pm UTC](https://discourse.rocq-prover.org/t/implicit-differentiation-in-coq-no-reals-no-limits-just-proof/2689 "2025-05-06T15:08:35Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![heliocoeur](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/heliocoeur/32/1113_2.png) [@heliocoeur](https://discourse.rocq-prover.org/u/heliocoeur)\
**Post date:** [May 6, 2025, 3:08pm UTC](https://discourse.rocq-prover.org/t/implicit-differentiation-in-coq-no-reals-no-limits-just-proof/2689/1 "2025-05-06T15:08:36Z")

</div>

# A Constructive, Symbolic Theory of Implicit Differentiation in Coq

## Overview:

This development presents a fully formal, self-contained theory of  
symbolic differentiation and implicit derivatives, built entirely  
within the Coq proof assistant.

Unlike external computer algebra systems, which manipulate expressions  
with opaque algorithms and approximations, this system is defined  
from first principles. All expressions, derivatives, and evaluations  
are constructed using inductive types and structural recursion.

It does not merely reimplement a known formula: it reconstructs, from  
syntactic primitives alone, the foundations of implicit differentiation  
without appealing to limits, real numbers, or classical analysis.  
This is not a simulation of calculus — it is a new, verifiable,  
syntax-driven theory of symbolic differentiation.

## Core Objectives:

1. Define symbolic expressions (`expr`) inductively as pure syntax.

2. Derive symbolic partial derivatives using a recursive function (`derive`).

3. Evaluate expressions under numerical environments (`eval_expr`).

4. Compute and verify implicit derivatives via the standard formula:

## Highlights:

✓ Every computation is symbolic, structural, and fully visible.  
✓ No use of real analysis, approximation, or external solvers.  
✓ The implicit derivative formula is not only computed but **proven**.  
✓ All steps are constructive and executed within the logic of Coq.  
✓ The system forms a minimal **syntactic theory of differentiation** ,  
abstract and extendable, independent of ℝ or limits.

## Comparison:

Unlike symbolic engines (e.g., SymPy, Mathematica), this approach:

- Is fully verifiable (proof-backed from the ground up).
- Exposes internal structure (expressions are inductive trees).
- Avoids heuristics (pure recursion on structure).
- Builds a foundation for certified mathematical computation.

## Main Theorem:

Let F(x, z, …) be a symbolic expression with variables assigned values,  
and suppose:

```
F(x, z, …) = 0 (i.e., the constraint holds at the point)
∂F/∂z ≠ 0 (non-degenerate Jacobian condition)

```

Then we prove, within Coq:

```
dz/dx = - (∂F/∂x) / (∂F/∂z)

```

The proof is constructive, relies only on symbolic syntax, and  
requires no reference to classical analysis.

```coq
Require Import String List ZArith.
Open Scope string_scope.
Open Scope Z_scope.
Import ListNotations.

(* --- Expressions symboliques --- *)
Inductive expr :=
| Var : string -> expr
| Const : Z -> expr
| Add : expr -> expr -> expr
| Mul : expr -> expr -> expr
| Pow : expr -> nat -> expr.

Definition valuation := list (string * Z).

Fixpoint lookup (x : string) (env : valuation) : Z :=
  match env with
  | [] => 0
  | (y, v) :: rest => if String.eqb x y then v else lookup x rest
  end.

Fixpoint eval_expr (e : expr) (env : valuation) : Z :=
  match e with
  | Var x => lookup x env
  | Const n => n
  | Add e1 e2 => eval_expr e1 env + eval_expr e2 env
  | Mul e1 e2 => eval_expr e1 env * eval_expr e2 env
  | Pow base n => Z.pow (eval_expr base env) (Z.of_nat n)
  end.

Fixpoint derive (v : string) (e : expr) : expr :=
  match e with
  | Var x => if String.eqb x v then Const 1 else Const 0
  | Const _ => Const 0
  | Add e1 e2 => Add (derive v e1) (derive v e2)
  | Mul e1 e2 => Add (Mul (derive v e1) e2) (Mul e1 (derive v e2))
  | Pow base n =>
      match n with
      | 0%nat => Const 0
      | S n' => Mul (Mul (Const (Z.of_nat n)) (Pow base n')) (derive v base)
      end
  end.

Definition eval_implicit_derivative_fraction
  (F : expr) (target var : string) (env : valuation) : Z * Z :=
  let num := eval_expr (derive var F) env in
  let denom := eval_expr (derive target F) env in
  (-num, denom).

(* --- Structure générale d’un système implicite --- *)
Record ImplicitSystem := {
  Fdef : expr;
  valuation_env : valuation;
  target_var : string; (* variable dépendante *)
  independent_var : string; (* variable par rapport à laquelle on dérive *)
  hypothesis_satisfied : eval_expr Fdef valuation_env = 0;
  hypothesis_nonzero : eval_expr (derive target_var Fdef) valuation_env <> 0
}.

(* --- Théorème généralisé --- *)
Theorem general_implicit_derivative_valid :
  forall (S : ImplicitSystem),
    eval_implicit_derivative_fraction S.(Fdef) S.(target_var) S.(independent_var) S.(valuation_env)
    =
    (- eval_expr (derive S.(independent_var) S.(Fdef)) S.(valuation_env),
     eval_expr (derive S.(target_var) S.(Fdef)) S.(valuation_env)).
Proof.
  intros [F env z x Hsat Hdz]. simpl. reflexivity.
Qed.

(* === Example: Explicit evaluation of dz/dx === *)

(* Define F(x, z) = x * z + z^2 *)
Definition F_example := Add (Mul (Var "x") (Var "z")) (Pow (Var "z") 2).

(* Define environment: x = 1, z = 2 *)
Definition env_example := [("x", 1); ("z", 2)].

(* Compute symbolic partial derivatives *)
Eval compute in derive "x" F_example. (* Should be z *)
Eval compute in derive "z" F_example. (* Should be x + 2z *)

(* Compute their evaluations under the environment *)
Eval compute in eval_expr (derive "x" F_example) env_example. (* → 2 *)
Eval compute in eval_expr (derive "z" F_example) env_example. (* → 1 + 4 = 5 *)

(* Compute dz/dx = - (∂F/∂x) / (∂F/∂z) *)
Eval compute in eval_implicit_derivative_fraction F_example "z" "x" env_example.
(* → (-2, 5) ⇒ dz/dx = -2/5 *)

```

```auto
coqtop < differential2.v
Welcome to Coq 8.20.0

Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < [Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]

Coq <
Coq <
Coq <
Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < expr is defined
expr_rect is defined
expr_ind is defined
expr_rec is defined
expr_sind is defined

Coq < Coq < valuation is defined

Coq < Coq < Coq < Coq < Coq < Coq < lookup is defined
lookup is recursively defined (guarded on 2nd argument)

Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < eval_expr is defined
eval_expr is recursively defined (guarded on 1st argument)

Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < derive is defined
derive is recursively defined (guarded on 2nd argument)

Coq < Coq < Coq < Coq < Coq < Coq < eval_implicit_derivative_fraction is defined

Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < ImplicitSystem is defined
Fdef is defined
valuation_env is defined
target_var is defined
independent_var is defined
hypothesis_satisfied is defined
hypothesis_nonzero is defined

Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < 1 goal

  ============================
  forall S : ImplicitSystem,
  eval_implicit_derivative_fraction (Fdef S) (target_var S)
    (independent_var S) (valuation_env S) =
  (- eval_expr (derive (independent_var S) (Fdef S)) (valuation_env S),
   eval_expr (derive (target_var S) (Fdef S)) (valuation_env S))

general_implicit_derivative_valid <
general_implicit_derivative_valid < 1 goal

  F : expr
  env : valuation
  z, x : string
  Hsat : eval_expr F env = 0
  Hdz : eval_expr (derive z F) env <> 0
  ============================
  eval_implicit_derivative_fraction
    (Fdef
       {|
         Fdef := F;
         valuation_env := env;
         target_var := z;
         independent_var := x;
         hypothesis_satisfied := Hsat;
         hypothesis_nonzero := Hdz
       |})
    (target_var
       {|
         Fdef := F;
         valuation_env := env;
         target_var := z;
         independent_var := x;
         hypothesis_satisfied := Hsat;
         hypothesis_nonzero := Hdz
       |})
    (independent_var
       {|
         Fdef := F;
         valuation_env := env;
         target_var := z;
         independent_var := x;
         hypothesis_satisfied := Hsat;
         hypothesis_nonzero := Hdz
       |})
    (valuation_env
       {|
         Fdef := F;
         valuation_env := env;
         target_var := z;
         independent_var := x;
         hypothesis_satisfied := Hsat;
         hypothesis_nonzero := Hdz
       |}) =
  (-
   eval_expr
     (derive
        (independent_var
           {|
             Fdef := F;
             valuation_env := env;
             target_var := z;
             independent_var := x;
             hypothesis_satisfied := Hsat;
             hypothesis_nonzero := Hdz
           |})
        (Fdef
           {|
             Fdef := F;
             valuation_env := env;
             target_var := z;
             independent_var := x;
             hypothesis_satisfied := Hsat;
             hypothesis_nonzero := Hdz
           |}))
     (valuation_env
        {|
          Fdef := F;
          valuation_env := env;
          target_var := z;
          independent_var := x;
          hypothesis_satisfied := Hsat;
          hypothesis_nonzero := Hdz
        |}),
   eval_expr
     (derive
        (target_var
           {|
             Fdef := F;
             valuation_env := env;
             target_var := z;
             independent_var := x;
             hypothesis_satisfied := Hsat;
             hypothesis_nonzero := Hdz
           |})
        (Fdef
           {|
             Fdef := F;
             valuation_env := env;
             target_var := z;
             independent_var := x;
             hypothesis_satisfied := Hsat;
             hypothesis_nonzero := Hdz
           |}))
     (valuation_env
        {|
          Fdef := F;
          valuation_env := env;
          target_var := z;
          independent_var := x;
          hypothesis_satisfied := Hsat;
          hypothesis_nonzero := Hdz
        |}))

1 goal

  F : expr
  env : valuation
  z, x : string
  Hsat : eval_expr F env = 0
  Hdz : eval_expr (derive z F) env <> 0
  ============================
  eval_implicit_derivative_fraction F z x env =
  (- eval_expr (derive x F) env, eval_expr (derive z F) env)

No more goals.

general_implicit_derivative_valid <
Coq < Coq < Coq < Coq < Coq < Coq < F_example is defined

Coq < Coq < Coq < env_example is defined

Coq < Coq < Coq < = Add (Add (Mul (Const 1) (Var "z")) (Mul (Var "x") (Const 0)))
         (Mul (Mul (Const 2) (Pow (Var "z") 1)) (Const 0))
     : expr

Coq < = Add (Add (Mul (Const 0) (Var "z")) (Mul (Var "x") (Const 1)))
         (Mul (Mul (Const 2) (Pow (Var "z") 1)) (Const 1))
     : expr

Coq < Coq < Coq < = 2
     : Z

Coq < = 5
     : Z

Coq < Coq < Coq < = (-2, 5)
     : Z * Z

Coq < Coq <

```

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [May 6, 2025, 3:21pm UTC](https://discourse.rocq-prover.org/t/implicit-differentiation-in-coq-no-reals-no-limits-just-proof/2689/2 "2025-05-06T15:21:07Z")

</div>

If you comment out `hypothesis_satisfied` and `hypothesis_nonzero` and adjust the `intros` tactic accordingly the theorem still holds.