Library NbSteps.nb_steps

Author: Jean-François Monin, Verimag, Université Grenoble Alpes

Graph free version of an example developed with Dominique Larchey-Wendling in the chapter book on the Braga method

Require Import Utf8 Extraction.

Target : nb of g steps to get some condition b

      let rec  ns x = match b x with true => 0 | false => S (ns (g x))

Algorithm using an accumulator

    let rec nsa x n = match b x with true => n | false => nsa (g x) (S n)

We prove that ns computes the same result as nsa.

Section ns_nsa.

Variable (X : Type) (g : X → X) (b : X → bool).

Unset Elimination Schemes.

Fact true_false {x} : x = true → x = false → False.
Proof. intros et. rewrite et. intros e; discriminate e. Qed.

The custom inductive domain of ns and nsa

This definition with x as an indice corresponds to the rules of the Braga paper

Inductive 𝔻 ns : X → Prop :=
| 𝔻 ns_tt : ∀x , b x = true → 𝔻 ns x
| 𝔻 ns_ff : ∀x , b x = false → 𝔻 ns (g x) → 𝔻 ns x
.

Small inversion (unused but good warming up)

Inductive is_𝔻 ns_tt x : 𝔻 ns x → Prop :=
| is_𝔻 ns_tt_intro e : is_𝔻 ns_tt x (𝔻 ns_tt x e).
Inductive is_𝔻 ns_ff x : 𝔻 ns x → Prop :=
| is_𝔻 ns_ff_intro e D : is_𝔻 ns_ff x (𝔻 ns_ff x e D).

Trick for dealing with this LISP-style definition: destruct (b x) before destruct D. The Coq tactic inversion D is unusable

Lemma 𝔻 ns_inv {x} (D : 𝔻 ns x) :
  match b x return 𝔻 ns x → Prop with
  | true ⇒ is_𝔻 ns_tt x
  | false ⇒ is_𝔻 ns_ff x
  end D.
Proof.
  destruct (b x) eqn:ebx; destruct D as [x e | x e D]; try constructor.
  - destruct (true_false ebx e).
  - destruct (true_false e ebx).
Qed.

The projection of constructor 𝔻ns_ff

Definition π _𝔻 ns {x} (D : 𝔻 ns x) : b x = false → 𝔻 ns (g x) :=
  match D with
  | 𝔻 ns_tt x E ⇒ λ G , match true_false E G with end
  | 𝔻 ns_ff x E Dgx ⇒ λ _, Dgx
  end.

Smaller inversion (crucial step for 𝔻ns_rect)

Inductive is_𝔻 ns_ff_π {x} (D : 𝔻 ns x) : 𝔻 ns x → Prop :=
| is_𝔻 ns_ff_π _intro e : is_𝔻 ns_ff_π D (𝔻 ns_ff x e (π _𝔻 ns D e)).

Lemma 𝔻 ns_π _inv {x} (D : 𝔻 ns x) :
  match b x as bx return 𝔻 ns x → 𝔻 ns x → Prop with
  | true ⇒ λ _, is_𝔻 ns_tt x
  | false ⇒ is_𝔻 ns_ff_π
  end D D.
Proof.

inversion D is unusable

  destruct (b x) eqn:ebx; destruct D as [x e | x e D]; try constructor.
  - destruct (true_false ebx e).
  - destruct (true_false e ebx).
Qed.

Set Elimination Schemes.

Definition of ns/nsa as structural fixpoints on the domain predicate

Fixpoint ns x (D : 𝔻 ns x) : nat :=
  match b x as bx return b x = bx → _ with
  | true ⇒ λ _, 0
  | false ⇒ λ G , S (ns (g x) (π _𝔻 ns D G))
  end eq_refl.

Fixpoint nsa x (n : nat) (D : 𝔻 ns x) : nat :=
  match b x as bx return b x = bx → _ with
  | true ⇒ λ _, n
  | false ⇒ λ G , nsa (g x) (S n) (π _𝔻 ns D G)
  end eq_refl.

Fixpoint equations are for free! Example

Example ns_fix_ff x E D : ns x (𝔻 ns_ff x E D) = S (ns (g x) D).
Proof. simpl; now rewrite E. Qed.

We can show the next equality by structural recursion on D

Lemma nsa_ns_n_direct : ∀x n D , nsa x n D = ns x D + n.
Proof.
  refine (fix loop x n D { struct D } := _).
  destruct D as [ x E | x E D ]; simpl.
  - now rewrite E.
  - now rewrite loop, E, <- plus_n_Sm.
Qed.

Corollary nsa_ns_direct : ∀x (D: 𝔻 ns x ), nsa x 0 D = ns x D.
Proof. intros; now rewrite nsa_ns_n_direct, plus_n_O. Qed.

An eliminator for 𝔻ns which follows the program scheme of ns and nsa

Theorem 𝔻 ns_rect
        (P : ∀x , 𝔻 ns x → Type)
        (Ptt : ∀x E , P _ (𝔻 ns_tt x E))
        (Pff : ∀x E D , P _ D → P _ (𝔻 ns_ff x E D)) :
  ∀ x D , P x D.
Proof.
  refine (
      fix loop x D {struct D} :=
        match b x as bx return b x = bx → _ with
        | true ⇒ λ E D , _
        | false ⇒ λ E D , _
        end eq_refl D);
    generalize (𝔻 ns_π _inv D); rewrite E; intros [].
  - apply Ptt.
  - apply Pff, loop.
Qed.

Application: Equality by dependent induction on D

Lemma nsa_ns_n x n D : nsa x n D = ns x D + n.
Proof.
  revert n.
  induction D as [ x e | x e D HD ] using 𝔻 ns_rect;
    intro n; cbn; rewrite e.
  - reflexivity.
  - cbn. rewrite HD, plus_n_Sm. reflexivity.
Qed.

End ns_nsa.

Extract Inductive bool ⇒ "bool" [ "true" "false" ].

Recursive Extraction ns nsa.