nm_correct.v

(**************************************************************)
(*   Copyright Dominique Larchey-Wendling    [*]              *)
(*             Jean-François Monin           [+]              *)
(*                                                            *)
(*            [*] Affiliation LORIA -- CNRS                   *)
(*            [+] Affiliation VERIMAG - Univ. Grenoble-Alpes  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** Using the simulated IR definition of 

              𝔻 : Ω -> Prop and nm : forall e, 𝔻 e -> Ω

    we show show partial correctness of nm:

      a) if De : 𝔻 e then nm e De is normal

      b) if De : 𝔻 e then nm e De is equivalent to e

    both by dependent induction on De : 𝔻 e
*)

Require Import Arith Omega Wellfounded.

Require Import nm_defs.

Set Implicit Arguments.

(* Now we show the partial correctness of nm, independently of its termination *)

(** normal forms only have atoms as boolean condition ie. b in if b then _ else _ *)

Inductive normal : Ω -> Prop :=
  | in_normal_0 : normal α
  | in_normal_1 : forall y z, normal y -> normal z -> normal (ω α y z).

Notation ℕ := normal.

(** nm produces normal forms *)

Theorem nm_normal e D : ℕ (nm e D).
Proof.
  induction D as [ e D1 D2 | | y z D1 ID1 D2 ID2 | u v w y z D1 ID1 D2 ID2 D3 ID3 ].
  - rewrite (nm_pirr _ D1); auto.
  - rewrite nm_fix_0; constructor.
  - rewrite nm_fix_1; constructor; auto.
  - rewrite nm_fix_2; auto.
Qed.

(** equiv is the congruence generated by ω (ω a b c) y z ~e ω a (ω b y z) (ω c y z) *)

Reserved Notation "x '~Ω' y" (at level 70, no associativity).

Inductive equiv : Ω -> Ω -> Prop :=
  | in_eq_0 : forall u v w y z, ω (ω u v w) y z ~Ω ω u (ω v y z) (ω w y z)
  | in_eq_1 : forall x x' y y' z z', x ~Ω x' -> y ~Ω y' -> z ~Ω z'-> ω x y z ~Ω ω x' y' z'
  | in_eq_2 : α ~Ω α
  | in_eq_3 : forall x y z, x ~Ω y -> y ~Ω z -> x ~Ω z
where "x ~Ω y" := (equiv x y).

Hint Constructors equiv.

Fact equiv_refl e : e ~Ω e.
Proof. induction e; auto. Qed.

Hint Resolve equiv_refl.

Notation equiv_trans := in_eq_3.

(** nm preserves equivalence *)

Fact nm_equiv e D : e ~Ω nm e D.
Proof.
  induction D as [ e D1 D2 | | y z D1 ID1 D2 ID2 | u v w y z D1 ID1 D2 ID2 D3 ID3 ].
  - rewrite (nm_pirr _ D1); auto.
  - rewrite nm_fix_0; auto.
  - rewrite nm_fix_1; auto.
  - rewrite nm_fix_2.
    apply equiv_trans with (2 := ID3),
          equiv_trans with (1 := in_eq_0 _ _ _ _ _); auto.
Qed.