On the danger of evaluation

First define on nat the exponential towers of base 2 and heigth n. For instance the tower of height 4 is 2222 =16384.
  1. Consider the following definition of even natural numbers:
    Inductive even : nat -> Prop :=
      even0 : even 0
    | even_S : forall p, even p -> even (S (S p)).
    Hint Constructors even.
    Prove that the tower of height 6 is an even number, and let us call your theorem six_tower.
  2. Try the command Eval compute in six_tower
  3. Make the constant six_tower transparent (by replacing its Qed with Defined), and redo the preceding question.
  4. I presume that your proof of six_tower uses some lemmas. Edit your proof and replace their Qed with Defined. What happens?


Look at this file .
Going home