Wellfounded induction was not neededHEADmaster

1 files changed, 3 insertions, 14 deletions

diff --git a/expr.v b/expr.v
index 2288b3a..e7970e2 100644
--- a/expr.v
+++ b/expr.v
@@ -1,4 +1,4 @@
-Require Import Omega Wellfounded Coq.Lists.List.
+Require Import Coq.Lists.List.
 Import ListNotations.
 
 Inductive Exp (v : Type) :=
@@ -61,25 +61,14 @@ Lemma correctness_partial_compilation (v : Type) (e : Exp v) :
   Some results = pn_eval v env rest ->
   Some (eval v env e :: results) = pn_eval v env (rev (rpn v e) ++ rest).
 Proof.
-
-Fixpoint exprsize (v : Type) (e : Exp v) : nat :=
-  match e with
-  | elit _ _ => 1
-  | evar _ _ => 1
-  | eadd _ a b => 1 + exprsize v a + exprsize v b
-  end.
-induction e using (well_founded_induction
-  (wf_inverse_image _ nat _ (exprsize v) PeanoNat.Nat.lt_wf_0)).
-
-intros.
-destruct e; simpl; try rewrite <- H0; try reflexivity.
+induction e; intros; simpl; try rewrite <- H; simpl; try reflexivity.
 rewrite (rev_app_distr (rpn v e2)).
 rewrite (rev_app_distr (rpn v e1)).
 simpl.
 rewrite (app_assoc_reverse (rev (rpn v e1)) (rev (rpn v e2)) rest).
 assert (Some (eval v env e1 :: eval v env e2 :: results)
     = pn_eval v env (rev (rpn v e1) ++ rev (rpn v e2) ++ rest)) as recstep.
-  apply H; try apply H; simpl; try assumption; omega.
+  apply IHe1. apply IHe2. assumption.
 rewrite <- recstep.
 reflexivity.
 Qed.