The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

I think the first two questions to ask are whether the proofs are similar and whether they are very long. If the proofs are similar, does that mean the addresses, the 1 and the 2 are not very significant in this case? If that's the case perhaps you can prove a theorem parametrized by those?

Thanks,
Jason Hu

On Feb 2, 2020 05:11, Gabriel Scherer  <gabriel.scherer AT gmail.com> wrote:

An first way to go about it would be to define an inductive to indicate which case is being considered (the naming is a bit silly in my example, but with your domain knowledge you can choose better names):

Inductive case :=

| Case1 : case

| Case2 : case

.

Definition ea_in_app_range case :=

  match case with

  | Case1 => ea_in_app1_range

  | Case2 => ea_in_app2_range

  end.

Definition CPUContextApp case :=

  match case with

  | Case1 => CPUContextApp1

  | Case2 => CPUContextApp2

  end.

Theorem app_access_self_ok :
    forall case (ea : Z),
        ea_in_app_range case ea ->
         let tlbe := find_tlbe (CPUContextApp case) ea TLB in
         (   tlb_hit tlbe
          /\ addr_translate_ok tlbe ea
          /\ access_granted (CPUContextApp case) tlbe).

This just a rephrasing of your statements with a simple factorization. It is useful if the proofs of the two theorems share a lot of logic which does not depend on the case (the parts of the proof that use case distinction are small).

Note that trying to write the proof in a higher-order style (abstracted over functions for ea_in_app_range and CPUContextApp) would be more powerful but is also going to be much harder: there is no chance for your theorem to hold for *any* function at their types, so you have to figure out what are the sufficient conditions on their choice for the theorem to hold. You get a stronger result (as long as the conditions are less restrictive than "being either foo1 or foo2") but it is much more work.

On Sun, Feb 2, 2020 at 10:32 AM 朱立平 <zlponline AT 163.com> wrote:

I have two(and may be more) theorems as follows and I don't think  proving them one by one is a good way.

Theorem app1_access_self_ok :

    forall (ea : Z),

        ea_in_app1_range ea ->

         let tlbe := find_tlbe CPUContextAPP1 ea TLB in

         (   tlb_hit tlbe

          /\ addr_translate_ok tlbe ea

          /\ access_granted CPUContextAPP1 tlbe).

Theorem app2_access_self_ok :

    forall (ea : Z),

        ea_in_app2_range ea ->

         let tlbe := find_tlbe CPUContextAPP2 ea TLB in

         (   tlb_hit tlbe

          /\ addr_translate_ok tlbe ea

          /\ access_granted CPUContextAPP2 tlbe).  

The differences are 

Definition ea_in_app1_range (ea : Z) : Prop :=   (to_Z "0x40040000") <= ea <=(to_Z "0x4004ffff") . 

Definition ea_in_app2_range (ea : Z) : Prop :=   (to_Z "0x40050000") <= ea <=(to_Z "0x4005ffff") .

and

Definition CPUContextAPP1 := mk_cpucontext true true true (1).

Definition CPUContextAPP2 := mk_cpucontext true true true (2).

Is there an elegant way to prove them in one theorem?  Will high-order be used in this scenario? Thanks!

Best,

Julian