मैं लाइब्रेरी प्रमेय लागू करना चाहता हूं:

Theorem Zplus_mod: forall a b n, (a + b) mod n = (a mod n + b mod n) mod n.

जहां a b n के प्रकार Z होने की उम्मीद है।

मेरे लक्ष्य में a b : nat के साथ एक उप-अभिव्यक्ति (a + b) mod 3 है।

rewrite Zplus_mod एक त्रुटि देता है Found no subterm matching

rewrite Zplus_mod with (a := a) एक त्रुटि देता है "a" has type "nat" while it is expected to have type "Z".

चूँकि प्राकृत संख्याएँ भी पूर्णांक होती हैं, नेट तर्कों के लिए Zplus_mod प्रमेय का उपयोग कैसे करें?

0
mercury0114 14 जून 2020, 15:10

1 उत्तर

सबसे बढ़िया उत्तर

आप इस प्रमेय को लागू नहीं कर सकते, क्योंकि संकेतन mod प्राकृतिक संख्याओं पर एक फ़ंक्शन को संदर्भित करता है Nat.modulo उस संदर्भ में जहां आप प्राकृतिक संख्याओं का उपयोग कर रहे हैं, जबकि संकेतन mod का संदर्भ Z.modulo जब आप Z प्रकार के पूर्णांकों की बात कर रहे हों।

Search कमांड का उपयोग करके आप विशेष रूप से Nat.modulo और (_ + _)%nat के बारे में प्रमेयों की खोज कर सकते हैं और आप देखेंगे कि कुछ मौजूदा प्रमेय वास्तव में आपकी आवश्यकताओं के करीब हैं (Nat.add_mod_idemp_l और Nat.add_mod_idemp_r).

आप Z.modulo और Nat.modulo को जोड़ने वाले प्रमेय की तलाश भी कर सकते हैं। यह mod_Zmod देता है। लेकिन यह आपको पूर्णांकों के प्रकार में काम करने के लिए मजबूर करता है:

Require Import Arith ZArith.

Search Z.modulo Nat.modulo.

 (* The answer is :  
    mod_Zmod: forall n m, m <> 0 -> Z.of_nat (n mod m) = 
       (Z.of_nat n mod Z.of_nat m)%Z  *)

इसका एक तरीका यह है कि आप एक ऐसे प्रमेय का पता लगाएं जो आपको बताता हो कि फंक्शन Z.of_nat इंजेक्टिव है। मैंने इसे निम्न आदेश टाइप करके पाया।

Search Z.of_nat "inj".

तैयार की गई लंबी सूची में, प्रासंगिक प्रमेय Nat2Z.inj है, आप फिर दिखाने की जरूरत है कि कैसे Z.of_nat शामिल सभी ऑपरेटरों के साथ इंटरैक्ट करता है। इनमें से अधिकांश प्रमेयों के लिए n गैर-शून्य होना आवश्यक है, इसलिए मैं इसे एक शर्त के रूप में जोड़ता हूं। यहाँ उदाहरण है।

Lemma example (a b n : nat) : 
   n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n.
Proof.
intro nn0.
apply Nat2Z.inj.
rewrite !mod_Zmod; auto.
rewrite !Nat2Z.inj_add.
rewrite !mod_Zmod; auto.
rewrite Zplus_mod.
easy.
Qed.

यह आपके प्रश्न का उत्तर देता है, लेकिन स्पष्ट रूप से, मेरा मानना ​​है कि आप नींबू Nat.add_mod_idemp_l और Nat.add_mod_idemp_r का उपयोग करना बेहतर समझते हैं।

1
Yves 15 जून 2020, 07:52