The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

Oh, the irony!

I have the following definition, a more or less direct copy of the
arith evaluator from Pierce's Types And Programming Languages:

--8<--

Require Import Coq.Strings.String.

Inductive term : Set :=
    Term_Zero   : term
  | Term_True   : term
  | Term_False  : term
  | Term_Succ   : term -> term
  | Term_Pred   : term -> term
  | Term_IsZero : term -> term
  | Term_Cond   : term -> term -> term -> term.

Fixpoint numeric (t : term) :=
  match t with
  | Term_Zero    => true
  | Term_Succ t0 => numeric t0
  | Term_Pred t0 => numeric t0
  | _            => false
  end.

Inductive result : Set :=
  | Result_NF    : term -> result
  | Result_Next  : term -> result
  | Result_Error : string -> result.

Fixpoint one_step (t : term) : result :=
  match t with
  (* 
   * values
   *)
  | Term_Zero  => Result_NF t
  | Term_True  => Result_NF t
  | Term_False => Result_NF t
  (*
   * iszero
   *)
  | Term_IsZero  Term_Zero     => Result_Next Term_True
  | Term_IsZero (Term_Succ t0) =>
    match numeric t0 with
    | true  => Result_Next Term_False
    | false => Result_Error "iszero applied to non-numeric value"
    end
  | Term_IsZero t0 =>
    match numeric t0 with
    | true =>
      match one_step t0 with
      | Result_NF t1   => Result_Next (Term_IsZero t1)
      | Result_Next t1 => Result_Next (Term_IsZero t1)
      | Result_Error s => Result_Error s
      end
    | false => Result_Error "iszero applied to non-numeric value"
    end
  (*
   * succ
   *)
  | Term_Succ t0 =>
    match numeric t0 with
    | true =>
      match one_step t0 with
      | Result_NF t1   => Result_NF (Term_Succ t1)
      | Result_Next t1 => Result_Next (Term_Succ t1)
      | Result_Error s => Result_Error s
      end
    | false => Result_Error "succ applied to non-numeric value"
    end
  (*
   * pred
   *)
  | Term_Pred Term_Zero      => Result_Next Term_Zero
  | Term_Pred (Term_Succ t0) =>
    match numeric t0 with
    | true  => Result_Next t0
    | false => Result_Error "pred applied to non-numeric value"
    end
  | Term_Pred t0 =>
    match numeric t0 with
    | true =>
      match one_step t0 with
      | Result_NF t1   => Result_Next (Term_Pred t1)
      | Result_Next t1 => Result_Next (Term_Pred t1)
      | Result_Error s => Result_Error s
      end
    | false => Result_Error "pred applied to non-numeric value"
    end
  (* 
   * if-then-else
   *)
  | Term_Cond Term_True t0 _  => Result_Next t0
  | Term_Cond Term_False _ t0 => Result_Next t0
  | Term_Cond tc t0 t1 =>
    match one_step t0 with
    | Result_NF tc1   => Result_Next (Term_Cond tc1 t0 t1)
    | Result_Next tc1 => Result_Next (Term_Cond tc1 t0 t1)
    | Result_Error s  => Result_Error s
    end
  end.

Definition error (r : result) :=
  match r with
  | Result_Error _ => true
  | _              => false
  end.

Lemma error_false : forall s,
  error (Result_Error s) = false -> False.
Proof.
  intros s H.
  inversion H.
Qed.

--8<--

Proving the three cases that do not terminate (in other words,
the evaluator raises an error) wasn't difficult:

--8<--

Definition result_subterm (r : result) (p : error r = false) : term :=
  (match r return (error r = false -> term) with
  | Result_Next t0 => fun _  => t0
  | Result_NF t0   => fun _  => t0
  | Result_Error s => fun p0 => False_rect _ (error_false s p0)
  end p).

Lemma succ_non_numeric : forall (t : term),
  numeric (Term_Succ t) = false -> numeric t = false.
Proof.
  intros t H0.
  trivial.
Qed.

Lemma succ_numeric : forall (t : term),
  numeric (Term_Succ t) = true -> numeric t = true.
Proof.
  intros t H0.
  trivial.
Qed.

Lemma pred_non_numeric : forall (t : term),
  numeric (Term_Pred t) = false -> numeric t = false.
Proof.
  intros t H0.
  trivial.
Qed.

Lemma pred_numeric : forall (t : term),
  numeric (Term_Pred t) = true -> numeric t = true.
Proof.
  intros t H0.
  trivial.
Qed.

Lemma numeric_ineq : forall (t0 t1 : term),
  (numeric t0 = false) -> (numeric t1 = true) -> t0 <> t1.
Proof.
  destruct t0, t1; try discriminate; congruence.
Qed.

Lemma succ_bool_stuck : forall (t : term),
  numeric t = false -> error (one_step (Term_Succ t)) = true.
Proof.
  intros t H.
  destruct t.
    (* case t = Term_Zero *)
    simpl; inversion H.
    (* case t = Term_True *)
    reflexivity.
    (* case t = Term_False *)
    reflexivity.
    (* case t = Term_Succ *)
    unfold one_step. rewrite succ_non_numeric. reflexivity. apply 
(succ_non_numeric t H).
    (* case t = Term_Pred *)
    unfold one_step. rewrite pred_non_numeric. reflexivity. apply 
(pred_non_numeric t H).
    (* case t = Term_IsZero *)
    trivial.
    (* case t = Term_Cond *)
    trivial.
Qed.

Lemma pred_bool_stuck : forall (t : term),
  numeric t = false -> error (one_step (Term_Pred t)) = true.
Proof.
  intros t H.
  destruct t.
    (* case t = Term_Zero *)
    simpl; inversion H.
    (* case t = Term_True *)
    reflexivity.
    (* case t = Term_False *)
    reflexivity.
    (* case t = Term_Succ *)
    unfold one_step. rewrite succ_non_numeric. reflexivity. apply 
(succ_non_numeric t H).
    (* case t = Term_Pred *)
    unfold one_step. rewrite pred_non_numeric. reflexivity. apply 
(pred_non_numeric t H).
    (* case t = Term_IsZero *)
    trivial.
    (* case t = Term_Cond *)
    trivial.
Qed.

Lemma iszero_bool_stuck : forall (t : term),
  numeric t = false -> error (one_step (Term_IsZero t)) = true.
Proof.
  intros t H.
  destruct t.
    (* case t = Term_Zero *)
    simpl; inversion H.
    (* case t = Term_True *)
    reflexivity.
    (* case t = Term_False *)
    reflexivity.
    (* case t = Term_Succ *)
    unfold one_step. rewrite succ_non_numeric. reflexivity. apply 
(succ_non_numeric t H).
    (* case t = Term_Pred *)
    unfold one_step. rewrite pred_non_numeric. reflexivity. apply 
(pred_non_numeric t H).
    (* case t = Term_IsZero *)
    trivial.
    (* case t = Term_Cond *)
    trivial.
Qed.

--8<--

However, I'm now stuck proving the first case that does terminate:

--8<--

Lemma pred_numeric_not_stuck : forall (t : term),
  numeric t = true -> error (one_step (Term_Pred t)) = false.
Proof.
  intros t H.
  induction t.
    (* case t = Term_Zero *)
    reflexivity.
    (* case t = Term_True *)
    inversion H.
    (* case t = Term_False *)
    inversion H.
    (* case t = Term_Succ *)
    unfold one_step. rewrite pred_numeric. reflexivity. apply (pred_numeric t 
H).
    (* case t = Term_Pred *)
    assert (numeric t = true) as Htn by apply (pred_numeric t H).

I have 'error (one_step (Term_Pred t)) = false' as an induction hypothesis 
but am
unable to prove 'error (one_step (Term_Pred (Term_Pred t))) = false' with it.

Any help would be appreciated (apologies for the size of the email, these 
definitions
are hard to shorten).