Wellfounded induction was not neededHEADmaster

2 files changed, 19 insertions, 37 deletions

diff --git a/expr.tex b/expr.tex
index 9e1ed34..591cde2 100644
--- a/expr.tex
+++ b/expr.tex
@@ -27,9 +27,9 @@ The \textsf{Exp} compiler, its semantics, the compiler and the proof
 	are formalised in Coq 8.6.
 The Coq file is attached to this report.
 The report walks through the file, but occasionally discusses things out of order when this aids understandability.
+The report is best followed with Coq alongside to see how the goals evolve.
 
-The proof uses well-founded induction, which is most easily done with the \textsf{Wellfounded} library.
-We also use \textsf{Omega} for basic arithmetic and the \textsf{ListNotations} module for pretty list notation.
+We only use one library, for dealing with lists.
 
 \coq{1}{2}
 
@@ -97,7 +97,7 @@ We now formally prove that the compiler in combination with the RPN evaluator ar
 In other words, for all variables types \textsf{v}, expressions \textsf{e} and environments \textsf{env},
 	the result of \textsf{rpn\_eval v env (rpn v e)} should be \textsf{Some (eval v env e)}.
 
-\coq{87}{88}
+\coq{76}{77}
 
 To prove this we first prove a lemma, operating on \textsf{pn\_eval} rather than \textsf{rpn\_eval}.
 Thus, we will show that the result of \textsf{pn\_eval v env (rev (rpn v e))} is \textsf{Some [eval v env e]}.
@@ -105,24 +105,19 @@ However, we will prove something more powerful: that this evaluation does not de
 Thus, if an arbitrary RPN program \textsf{rest} evaluates to the stack \textsf{results} when starting with an empty stack,
 	\textsf{pn\_eval v env (rev (rpn v e) ++ rest)} should be \textsf{Some (eval v env e :: results)}.
 
-\coq{59}{63}
-
-The proof is by well-founded induction on expressions.
-For this to work, we first provide a mapping \textsf{Exp v $\rightarrow$ nat} based on the size of expressions.
-Thus, there is some \enquote{ever decreasing score} that can be attributed to expressions, making the induction sound.
-
-\coq{65}{72}
+\coq{59}{62}
 
+The proof is by induction on expressions.
 After introducing the hypotheses, we make a case distinction over \textsf{e}.
 The cases for literals and variables are very similar and can be handled by applying the induction hypothesis.
 After this, only the case for addition is left.
 
-\coq{74}{75}
+\coq{63}{64}
 
 We now have an RPN program with \textsf{rpnadd} as the last instruction.
 Since the program is reversed for use in \textsf{pn\_eval}, we can rewrite the program to get \textsf{rpnadd} at its head.
 
-\coq{76}{78}
+\coq{65}{67}
 
 Suppose the original expression was \textsf{e = eadd e1 e2},
 	we now consider \textsf{pn\_eval v env ((rev (rpn v e1) ++ rev (rpn v e2)) ++ rest)}
@@ -131,31 +126,29 @@ Due to associativity of \textsf{++}, we can reanalyse this as
 	\textsf{pn\_eval v env (rev (rpn v e1) ++ (rev (rpn v e2) ++ rest))},
 	which allows for application of the induction hypothesis with \textsf{rev (rpn v e2) ++ rest} as the \enquote{rest of the program}, i.e., the \textsf{rest}.
 
-\coq{79}{81}
+\coq{68}{68}
 
-To be able to use the induction hypothesis on \textsf{e1} we have to show that it is strictly smaller than \textsf{eadd e1 e2}.
-This is easily done with \textsf{simpl} and \textsf{omega}.
-We then apply the induction hypothesis again for \textsf{e2} with \textsf{rest}.
-Here too, \textsf{simpl} and \textsf{omega} make the induction sound.
+Instead of getting the goal into the right shape, we \textsf{assert} a property that combines the two induction hypotheses
+	(one for \textsf{e1} and one for \textsf{e2}).
 We carry over the fact that \textsf{rest} results in \textsf{results} from the induction hypothesis using \textsf{assumption}.
 
-\coq{82}{82}
+\coq{69}{71}
 
 The proof of the lemma now follows by applying the assertion of the induction step.
 
-\coq{83}{85}
+\coq{72}{74}
 
 We now return to the proof of the correctness theorem:
 
-\coq{87}{89}
+\coq{76}{77}
 
-We outsource this proof to our proof on \textsf{pn\_eval} using \textsf{rest = result = []}.
+We outsource this proof to our lemma on \textsf{pn\_eval} using \textsf{rest = result = []}.
 
-\coq{90}{93}
+\coq{78}{82}
 
 The result of the call to \textsf{pn\_eval} from \textsf{rpn\_eval} is now known,
 	and we can simplify the \textsf{rpn\_eval} call further to the point of reflexivity.
 
-\coq{94}{97}
+\coq{83}{86}
 
 \end{document}
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.