🐛 Use constructive logic only for the warmup exercises

Turns out that decidability in coq is abbreviated as "dec" (which I initially understood as "decrement")

theories/type_systems/warmup/warmup.v

@@ -244,14 +244,6 @@ Fixpoint expr_eval' (m: gmap string Z) (e : expr') : Z :=
   | Mul' e1 e2 => (expr_eval' m e1) * (expr_eval' m e2)
   end.
 
-(*
-  I do not know how to prove the following proof using constructive logic only.
-  One could probably do so by transforming the rhs
-  until they get to an equivalent expression to the lhs.
-*)
-
-Require Import Classical_Prop.
-
 (* Prove the following lemma which explains how substitution interacts with evaluation *)
 Lemma eval_subst_extend (m: gmap string Z) e x e':
   expr_eval' m (subst e x e') = expr_eval' (<[x := expr_eval' m e']> m) e.
@@ -259,8 +251,10 @@ Proof.
   induction e as [ y | y | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2 ].
   -
     simpl.
-    destruct (classic (x = y)) as [H_eq | H_neq].
+    (* Use the decidability of bool to inspect both possibilities *)
+    destruct (bool_dec (bool_decide (x=y)) true) as [H_eq | H_neq].
     (* If x = y *)
+    apply bool_decide_eq_true in H_eq.
     rewrite <- decide_bool_decide; rewrite decide_True.
     rewrite H_eq.
     rewrite lookup_insert.
@@ -270,6 +264,8 @@ Proof.
     assumption.
 
     (* If x ≠ y *)
+    apply not_true_is_false in H_neq.
+    apply bool_decide_eq_false in H_neq.
     rewrite <- decide_bool_decide; rewrite decide_False; simpl.
     rewrite lookup_insert_ne.
     reflexivity.