What is the best way to proove a lemma with fixpoint definition?

I have a definition with fixpoint like this
Fixpoint find_tlbe (cxt : CPUContext) (ea : int) (b : TLB) : tlbe_option :=
match b with
| empty => None
| record tlbe b’ => if (V tlbe)
&& (negb (xorb (MSR_DS cxt) (TS tlbe)))
&& (Int.eq (PID cxt) (TID tlbe) || Int.eq (PID cxt) Int.zero)
&& (Int.eq (get_pn_from_epn (EPN tlbe)) (get_pn_from_ea ea) )
then (Some tlbe)
else (find_tlbe cxt ea b’)
end.

I got stuck when prove a lemma when using unfold tatic with it. Can anyone give me some example on this?

And further, the whole coq model can be found here:https://github.com/JulianXian/addr_trans/blob/master/addr_trans.v
Is it well founded? Thank you for your time.

Are you sure the problem is with fixpoints? Doesn’t the fixpoint get simplified away in your lemma os_access_tlbe_always_hit, leaving you with a sequence of if?

I imagine the goal looks like this:

H' : (if ... then (Some tlbe2) else
        if ... then (Some tlbe1) else
          if ... then (Some tlbe1) else None) = None
================================================
False

So you have to work through the conditions to find that at least one must be true.


You could simplify the current proof script a bit by removing the unfold find_tlbe in H' on line 295, but that won’t change the state you’re in (where the proof is Admitted).

As a general rule of thumb, never unfold fixpoints, and instead use destruct, induction or rewrite in order to get a constructor in the decreasing argument, and simplify by simpl/cbn. But in your case you already have a concrete argument.

I have removed the inappropriate using of unfold, and come to the following goal:
1 subgoals
ea : int
H : Int.le (Int.repr (to_Z “40000000”)) ea &&
Int.le ea (Int.repr (to_Z “4000FFFF”)) = true
H’ : (if (Int.eq (Int.repr 255) (Int.repr 255)
|| Int.eq (Int.repr 255) Int.zero) &&
Int.eq (Int.shru (Int.repr 1048576) (Int.repr 6))
(Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
then Some tlbe0
else None) = None
______________________________________(1/1)
False

H means that effective address (ea) in the range from 40000000 to 4000ffff, and the if statement in H’ is satisfied. I am realizing that I have used the fixpoint in a concrete case rather than a general one. Despite this , can I have a way to make this proof go on?

Dear Julian,

this would be easier to answer if you would give more information on where your “Int” module comes from. It looks quite like (https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v) but in the version I am using (3.5 and master) there is no le function. Without knowing what library you are using one cannot tell what facilities this library might have to solve such goals. Easiest (and most polite) is to supply a snippet of Coq code which can be run + information on versions you are using.

In case you are using something similar to the CompCert Integers library, a good way to do partial simplifications on constant terms is the change tactic, which can replace any terms which eventually compute to the same thing. cbn in H does nothing and compute in H probably doesn’t give you what you want. With change you get this far on a simplified goal (because I don’t have le):

Require Import compcert.lib.Integers.
Require Import ZArith.
Require Import Bool.

Goal
forall (tlbe0:int),
forall (ea:int),
(if (Int.eq (Int.repr 255) (Int.repr 255)
|| Int.eq (Int.repr 255) Int.zero) &&
Int.eq (Int.shru (Int.repr 1048576) (Int.repr 6))
(Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
then Some tlbe0
else None) = None
->
False.
Proof.
intros.
change (Int.eq (Int.repr 255) (Int.repr 255)) with true in H. cbn in H.
change (Int.shru (Int.repr 1048576) (Int.repr 6)) with (Int.repr 16384) in H.

results in

1 subgoal
tlbe0, ea : int
H : (if Int.eq (Int.repr 16384) (Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
     then Some tlbe0
     else None) = None
______________________________________(1/1)
False

I am not aware of any automated tool which can handle inequalities and bit operations, so I guess you have to see what Search Int.shru gives you. May be you can convert the shru to a division in Nat or Z and convert the goal with ring tactics to something lia can solve. But I would think this is a common thing for you, so I would prove some useful lemmas for this.

Best regards,

Michael

1 Like

Thank you for you kind answer, Michael.

The “Int” module here comes from Compcert 2.7 except that I had an le function added.
Definition le (x y: int) : bool :=
if zle (signed x) (signed y) then true else false.
(I wonder why there’s no such a commonly used funtion, even in version 3.5).
I have uploaded the modified code to https://github.com/JulianXian/addr_trans/blob/master/Integers.v
and other files can be found here. https://github.com/JulianXian/addr_trans/
The code can run on coq 8.4pl6, a version without tactic cbn. It seems simpl do the same thing.

I’m trying to learn more tactics and prove techniques to make the coq model more accurate.

Best,
Julian

Dear Julian,

unless you want to do very minor experiments with an existing development, there is no justification I can think of for using Coq 8.4pl6 and CompCert 2.7. You will be pretty much on your own with this version pick.

If you need additional functions, it is better to have your own IntExt module you can share with others rather than changing CompCert. This makes it easier for others to help you. If you think your functions are generally useful, you should do a PR to CompCert.

Best regards,

Michael

I’m ready for upgrading to the latest version of Coq and Compcert.

In order to use original Compcert Intergers library, I change my goal to a tempopary goal
______________________________________(1/2)
Int.lt (Int.repr (to_Z “3fffffff”)) ea &&
Int.lt ea (Int.repr (to_Z “40010000”)) = true ->
Int.eq (Int.repr 16384)
(Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535)) = true

and a final goal like:
H1:P: Prop
H2: (if Q
then Some tlbe0
else None) == None
H3:P->Q
______________________________________(2/2)
False.

Is that a reasonable choice?