DPM-NBE

Experiments on implementing Dependent Pattern Matching under Normalization by Evaluation setup.

Syntax

Example

let trans : (A : U) (a b c : A) -> Id A a b -> Id A b c -> Id A a c =
  λ A a b c refl refl . refl; 

let cong : (A B : U) (f : A -> B) (a b : A) -> Id A a b -> Id B (f a) (f b) =
  λ A B f a b refl . refl;

let H : (m n : Nat) -> Id Nat n (plus m zero) -> Id Nat m zero -> Id Nat n zero =
  λ m n refl refl . refl;

let C : (A : U) -> Id Nat (suc zero) zero -> A = 
  λ A (!); -- Absurd pattern

U

Note.

• plus, suc, Id must be fully applied.
• For simplicity, we only have refl , absurd pattern (!) and variables as patterns, zero and suc is not a pattern. It is just to show DEPENDENT pattern matching.

Difficulty of DPM under NbE

The problem is that, for example, when we checking the following pattern matching

let H : (m n : Nat) -> Id Nat n (plus m zero) -> Id Nat m zero -> ... 
  λ m n refl refl . ...  

For the first refl, we need to unify n with plus m zero, extending the evaluation environment with n = plus m zero, which is a value (corresponding to a normal form). But the second refl gives m = zero, which makes the plus m zero [zero/m] no more a normal form.

Acknowledgements

• The base code is directly copied from András Kovács' elaboration zoo.

• The idea of the solution to DPM under NbE problem is also directly from Kovács' cctt and his talk, using explicit substitutions and forcing.

• The unification algorithm for solving the unification problems generated by DPM is from Ulf Norell's thesis and Jesper Cockx Dominique Devriese Frank Piessens' Pattern Matching Without K. Note that I do "with-K" here, but it is not a problem to change to "without-K".