The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Everyone,

I have a module type Schnorr_Group and I want to prove some properties about it. I therefore defined another module Schnorr_Properties and passed the Schnorr_Group as a parameter. So far everything is good, but if you look at the proof p_pos, you can see that I need to bring all the axioms of Schnorr_Group by using  'pose proof ..' mechanism for lia to be successful, and I found it very cumbersome.

My question: is there a way to get a very similar behaviour of  'Section' and 'Variable' in Module?

(What I mean by 'Section' and 'Variable' behaviour is that everything defined using Variable in a Sections is always present in the context, as long as the Section is open.)

Best,

Mukesh

Module Type Schnorr_Group.
(* p = k * q + 1 where p and q are prime *)
(* g is group generator of order q, g^q = 1 mod p *)
(* 2 <= k *)
(* t is random number from Zp *)
(* x is private key from Zq *)
(* h is public key from Zp *)
Parameters
(p q k g t x h : Z).

Axiom prime_p : prime p.
Axiom prime_q : prime q.
Axiom k_gteq_2 : 2 <= k.
Axiom safe_prime : p = k * q + 1.
Axiom ht : 1 < t < p.
Axiom hg : g = Zpow_mod t k p.
Axiom hg_neq_one : g <> 1.
Axiom hprivate : 1 < x < q.
Axiom hpublic : h = Zpow_mod g x p.
End Schnorr_Group.


(* Proof that g is a generator of order q *)
Module Schnorr_Properties (Import SG : Schnorr_Group).

I want to do some magic here to get all the parameters and Axioms of SG in this context.

Lemma p_pos : 0 < p.
Proof.
  pose proof prime_p as Hp.
  pose proof prime_q as Hq.
  pose proof k_gteq_2 as Hk.
  pose proof safe_prime as Hs.
  pose proof ht as Ht.
  pose proof hg as Hg.
  pose proof hg_neq_one as Hgn.
  pose proof hprivate as Hx.
  pose proof hpublic as Hh.
  lia.
Qed.

(* more theorems *)
End Schnorr_Properties.