CODEWITHSUNDEEP
coqtheorem-proving
Mohamed Elsheikh
Mohamed Elsheikh

Reputation: 3

Cannot rewrite in goal using Equations Package in Coq?

I am using Equations Package in coq , and currently I have this expression in my goal:

evalMS (if_then_else (if_then_else t1_1 t1_2 t1_3) t4 t5)

and this in my context

H: None = evalS (if_then_else t1_1 t1_2 t1_3)

i wnat to evalute the first expression, but I can't figure it out. first I used simp evalMS. and got

evalMS_unfold_clause_1 (if_then_else t1_1 t1_2 t1_3)
  (inspect (evalS (if_then_else t1_1 t1_2 t1_3))) t4 t5

then when I try rewrite <- H. I get this error

Abstracting over the term "evalS (if_then_else t1_1 t1_2 t1_3)" leads to a term
fun o : option FCPLang =>
evalMS_unfold_clause_1 (if_then_else t1_1 t1_2 t1_3) (inspect o) t4 t5 =
evalBS (if_then_else (if_then_else t1_1 t1_2 t1_3) t4 t5)
which is ill-typed.
Reason is: Illegal application: 
The term "evalMS_unfold_clause_1" of type
 "forall t1 : FCPLang,
  {b : option FCPLang | evalS t1 = b} -> FCPLang -> FCPLang -> option FCPLang"
cannot be applied to the terms
 "if_then_else t1_1 t1_2 t1_3" : "FCPLang"
 "inspect o" : "{b : option FCPLang | o = b}"
 "t4" : "FCPLang"
 "t5" : "FCPLang"
The 2nd term has type "{b : option FCPLang | o = b}" which should be a subtype of
 "{b : option FCPLang | evalS (if_then_else t1_1 t1_2 t1_3) = b}".

Also this my definition of evalMS:

Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl.
Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
(*This definition tells Coq we'll prove the well-foundedness wf by showing that
the (measure term) will decrease (lt).*)
Equations? evalMS (term : FCPLang) : (option FCPLang) by wf (measure term) lt :=
evalMS (if_then_else t1 t2 t3) with inspect (evalS t1) => {
| Some (b true) eqn: eq1 => evalMS t2;
| Some (b false) eqn: eq2 => evalMS t3;
| Some (n n0) eqn:eq3 => None;
| Some A' eqn: eq4 => evalMS (if_then_else A' t2 t3);
| _ => None
};
evalMS (n C) := Some (n C);
evalMS (b B) := Some (b B).
- apply PeanoNat.Nat.lt_succ_r. rewrite (PeanoNat.Nat.add_comm (measure t1)). rewrite Arith_prebase.plus_assoc_reverse_stt. apply PeanoNat.Nat.le_add_r.
- apply PeanoNat.Nat.lt_succ_r. rewrite (PeanoNat.Nat.add_comm). apply PeanoNat.Nat.le_add_r.
- destruct t1. * discriminate eq4. * discriminate eq4.
* simpl. apply decreasing_measure in eq4. simpl in eq4. apply Arith_prebase.lt_n_S_stt. apply Arith_prebase.lt_n_S_stt. apply Arith_prebase.lt_S_n in eq4.
rewrite Arith_prebase.plus_assoc_reverse_stt. rewrite (PeanoNat.Nat.add_comm (measure f + measure f0 + measure f1)).
rewrite (Arith_prebase.plus_assoc_reverse_stt (measure t1_1 + measure t1_2 + measure t1_3)). rewrite (PeanoNat.Nat.add_comm (measure t1_1 + measure t1_2 + measure t1_3)).
apply Plus.plus_lt_compat_l_stt. assumption. Qed.

Upvotes: 0

Views: 45

Answers (2)

larsr
larsr

Reputation: 5811

Are you sure your definition is correct?

Perhaps your program should be like the one below. It doesn't consider the case if an evaluation leads to if_then_else (if_then_else t11 t12 t13) t2 t3) because that should not be possible if the computation of (if_then_else t11 t12 t13) is not stuck.

From Equations Require Import Equations.
From Coq Require Import List Arith Nat Lia.

Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl.
Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
(*This definition tells Coq we'll prove the well-foundedness wf by showing that
the (measure term) will decrease (lt).*)

Inductive FCPLang :=
| b (b:bool)
| n (n:nat)
| if_then_else (t1 t2 t3 :FCPLang)
.

Equations measure (f:FCPLang) : nat :=
| if_then_else t1 t2 t3  => 1 +  measure t1 + measure t2 + measure t3
| _ => 0.

Equations evalS (t:FCPLang) : option FCPLang :=
| _ => Some t.

Equations evalMS (term : FCPLang) : (option FCPLang) by wf (measure term) lt :=
evalMS (n C) => Some (n C);
evalMS (b B) => Some (b B);
evalMS (if_then_else (b true) t2 t3) => evalMS t2;
evalMS (if_then_else (b false) t2 t3) => evalMS t3;
evalMS _ => None.

Next Obligation.
rewrite measure_equation_3. lia.
Defined.

Next Obligation.
rewrite measure_equation_3. lia.
Defined.

Upvotes: 0

Thomas Lamiaux
Thomas Lamiaux

Reputation: 141

Could you edit your question to provide a MWE that works when copied and pasted so that it can be tried out ? It is very hard (sometimes impossible) to debug without trying it out.

Could you also specify which version of Equations you are using ? Some stuffs like handling of with clause have been improved in Equations 8.20.

Otherwise, all I can see is that it seems like a dependency issue. You are trying to rewrite a variable but another depends on it or sth like that, so I don't think it is an issue with Equations. You can try to unfold / destruct inspect first to see what is going on.

Upvotes: 0

Related Questions