From 19bb4b82381e664e368cb5b21ed5a4f7233f4aae Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Thu, 26 Oct 2023 16:49:51 +0200 Subject: [PATCH] :bug: 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 | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/theories/type_systems/warmup/warmup.v b/theories/type_systems/warmup/warmup.v index 5b2ac27..097dab3 100644 --- a/theories/type_systems/warmup/warmup.v +++ b/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.