# HG changeset patch # User Adam Chlipala # Date 1332955250 14400 # Node ID 252ba054a1cd7de889853c1db01f110b3eff5ec3 # Parent 3b36b1e05b4ee1451c4eb7a2eac5c75d6cdc108d One more example of avoiding axioms (getNat) diff -r 3b36b1e05b4e -r 252ba054a1cd src/Universes.v --- a/src/Universes.v Mon Mar 26 17:00:34 2012 -0400 +++ b/src/Universes.v Wed Mar 28 13:20:50 2012 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2009-2011, Adam Chlipala +(* Copyright (c) 2009-2012, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -8,6 +8,8 @@ *) (* begin hide *) +Require Import List. + Require Import DepList CpdtTactics. Set Implicit Arguments. @@ -1016,4 +1018,152 @@ Closed under the global context >> -This example illustrates again how some of the same design patterns we learned for dependently typed programming can be used fruitfully in theorem statements. *) +This example illustrates again how some of the same design patterns we learned for dependently typed programming can be used fruitfully in theorem statements. + +%\medskip% + +To close the chapter, we consider one final way to avoid dependence on axioms. Often this task is equivalent to writing definitions such that they %\emph{%##compute##%}%. That is, we want Coq's normal reduction to be able to run certain programs to completion. Here is a simple example where such computation can get stuck. In proving properties of such functions, we would need to apply axioms like %\index{axiom K}%K manually to make progress. + +Imagine we are working with %\index{deep embedding}%deeply embedded syntax of some programming language, where each term is considered to be in the scope of a number of free variables that hold normal Coq values. To enforce proper typing, we will need to model a Coq typing environment somehow. One natural choice is as a list of types, where variable number [i] will be treated as a reference to the [i]th element of the list. *) + +Section withTypes. + Variable types : list Set. + + (** To give the semantics of terms, we will need to represent value environments, which assign each variable a term of the proper type. *) + + Variable values : hlist (fun x : Set => x) types. + + (** Now imagine that we are writing some procedure that operates on a distinguished variable of type [nat]. A hypothesis formalizes this assumption, using the standard library function [nth_error] for looking up list elements by position. *) + + Variable natIndex : nat. + Variable natIndex_ok : nth_error types natIndex = Some nat. + + (** It is not hard to use this hypothesis to write a function for extracting the [nat] value in position [natIndex] of [values], starting with two helpful lemmas, each of which we finish with [Defined] to mark the lemma as transparent, so that its definition may be expanded during evaluation. *) + + Lemma nth_error_nil : forall A n x, + nth_error (@nil A) n = Some x + -> False. + destruct n; simpl; unfold error; congruence. + Defined. + + Implicit Arguments nth_error_nil [A n x]. + + Lemma Some_inj : forall A (x y : A), + Some x = Some y + -> x = y. + congruence. + Defined. + + Fixpoint getNat (types' : list Set) (values' : hlist (fun x : Set => x) types') + (natIndex : nat) : (nth_error types' natIndex = Some nat) -> nat := + match values' with + | HNil => fun pf => match nth_error_nil pf with end + | HCons t ts x values'' => + match natIndex return nth_error (t :: ts) natIndex = Some nat -> nat with + | O => fun pf => + match Some_inj pf in _ = T return T with + | refl_equal => x + end + | S natIndex' => getNat values'' natIndex' + end + end. +End withTypes. + +(** The problem becomes apparent when we experiment with running [getNat] on a concrete [types] list. *) + +Definition myTypes := unit :: nat :: bool :: nil. +Definition myValues : hlist (fun x : Set => x) myTypes := + tt ::: 3 ::: false ::: HNil. + +Definition myNatIndex := 1. + +Theorem myNatIndex_ok : nth_error myTypes myNatIndex = Some nat. + reflexivity. +Defined. + +Eval compute in getNat myValues myNatIndex myNatIndex_ok. +(** %\vspace{-.15in}%[[ + = 3 +]] + +We have not hit the problem yet, since we proceeded with a concrete equality proof for [myNatIndex_ok]. However, consider a case where we want to reason about the behavior of [getNat] %\emph{%##independently##%}% of a specific proof. *) + +Theorem getNat_is_reasonable : forall pf, getNat myValues myNatIndex pf = 3. + intro; compute. +(** +<< +1 subgoal +>> +%\vspace{-.3in}%[[ + pf : nth_error myTypes myNatIndex = Some nat + ============================ + match + match + pf in (_ = y) + return (nat = match y with + | Some H => H + | None => nat + end) + with + | eq_refl => eq_refl + end in (_ = T) return T + with + | eq_refl => 3 + end = 3 +]] + +Since the details of the equality proof [pf] are not known, computation can proceed no further. A rewrite with axiom K would allow us to make progress, but we can rethink the definitions a bit to avoid depending on axioms. *) + +Abort. + +(** Here is a definition of a function that turns out to be useful, though no doubt its purpose will be mysterious for now. A call [update ls n x] overwrites the [n]th position of the list [ls] with the value [x], padding the end of the list with extra [x] values as needed to ensure sufficient length. *) + +Fixpoint copies A (x : A) (n : nat) : list A := + match n with + | O => nil + | S n' => x :: copies x n' + end. + +Fixpoint update A (ls : list A) (n : nat) (x : A) : list A := + match ls with + | nil => copies x n ++ x :: nil + | y :: ls' => match n with + | O => x :: ls' + | S n' => y :: update ls' n' x + end + end. + +(** Now let us revisit the definition of [getNat]. *) + +Section withTypes'. + Variable types : list Set. + Variable natIndex : nat. + + (** Here is the trick: instead of asserting properties about the list [types], we build a %``%#"#new#"#%''% list that is %\emph{%##guaranteed by construction##%}% to have those properties. *) + + Definition types' := update types natIndex nat. + + Variable values : hlist (fun x : Set => x) types'. + + (** Now a bit of dependent pattern matching helps us rewrite [getNat] in a way that avoids any use of equality proofs. *) + + Fixpoint getNat' (types'' : list Set) (natIndex : nat) + : hlist (fun x : Set => x) (update types'' natIndex nat) -> nat := + match types'' with + | nil => fun vs => hhd vs + | t :: types0 => + match natIndex return hlist (fun x : Set => x) + (update (t :: types0) natIndex nat) -> nat with + | O => fun vs => hhd vs + | S natIndex' => fun vs => getNat' types0 natIndex' (htl vs) + end + end. +End withTypes'. + +(** Now the surprise comes in how easy it is to %\emph{%##use##%}% [getNat']. While typing works by modification of a types list, we can choose parameters so that the modification has no effect. *) + +Theorem getNat_is_reasonable : getNat' myTypes myNatIndex myValues = 3. + reflexivity. +Qed. + +(** The same parameters as before work without alteration, and we avoid use of axioms. *)