L. Paulson's If-Then-Else normalisation algorithm in Coq via simulated Induction-Recursion
CoqLGPL-2.1
L. Paulson's If-Then-Else normalisation in Coq
Copyright
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* Jean-François Monin [+] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(* [+] Affiliation VERIMAG - Univ. Grenoble *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
What is this repository for?
This repository is a Coq implementation and total correctness
proof of L. Paulson If-Then-Else normalisation which is a nested
recursive algorithm with a complicated scheme.
The proof of partial correctness and termination is postponed after
the domain and function have been defined together which their
constructors, induction principle, proof-irrelevance and fixpoint equations,
simulating the following Inductive-Recursive definition:
Inductive Ω : Set := α : Ω | ω : Ω -> Ω -> Ω -> Ω.
Inductive 𝔻 : Ω -> Prop :=
| d_nm_0 : 𝔻 α
| d_nm_1 : forall y z, 𝔻 y -> 𝔻 z -> 𝔻 (ω α y z)
| d_nm_2 : forall a b c y z (Db : 𝔻 (ω b y z)) (Dc : 𝔻 (ω c y z)),
𝔻 (ω a (nm (ω b y z) Db) (nm (ω c y z) Dc))
-> 𝔻 (ω (ω a b c) y z)
withFixpoint nm e (De : 𝔻 e) : Ω := match De with
| d_nm_0 => α
| d_nm_1 y z Dy Dz => ω α (nm y Dy) (nm z Dz)
| d_nm_2 a b c y z Db Dc Da => nm (ω a (nm (ω b y z) Db) (nm (ω c y z) Dc)) Da
end.