coq ट्यूटोरियल
Coq के साथ शुरुआत करना

टिप्पणियों

Coq का परीक्षण और स्थापना

स्थापित किए बिना परीक्षण

नए उपयोगकर्ताओं के लिए जो अपनी मशीन पर इसे स्थापित किए बिना Coq का परीक्षण शुरू करना चाहते हैं, एक ऑनलाइन IDE है जिसे JsCoq ( यहां प्रस्तुति) कहा जाता है । पैकेज उप-विंडो विभिन्न प्रसिद्ध पैकेजों का परीक्षण करने की अनुमति देता है।

स्थापना

डाउनलोड पृष्ठ में विंडोज और मैकओएस के लिए इंस्टॉलर हैं।

लिनक्स के उपयोगकर्ताओं को आमतौर पर नवीनतम संस्करण प्राप्त करने के लिए, ओपम का उपयोग करने वाले स्रोत से संकलन करने की सलाह दी जाती है। ऐसा करने के लिए बुनियादी निर्देश यहां दिए गए हैं ।

एक साधारण सा प्रमाण

Theorem my_first_theorem : 1 + 1 = 2.
Proof.
  reflexivity.
Qed.

इसे अपने ब्राउज़र में आज़माएं ।

MacOS पर Coq स्थापित करें

आप यहाँ से dmg पैकेज डाउनलोड करके पूरे बंडल को स्थापित कर सकते हैं ।

बंडल में एक CoIDEIDE है जिसका उपयोग आपके प्रमाण लिखने के लिए किया जा सकता है या आप अपने टर्मिनल पर दुभाषिया को चलाने के लिए coqtop कमांड का उपयोग कर सकते हैं

MacOS पर Coq की स्थापना होमब्रे का उपयोग करना आसान है

brew install coq

या यदि आप MacPorts का उपयोग करते हैं

sudo port install coq

Coq के लिए कोई अच्छा vi समर्थन नहीं है। आप Emacs के भीतर प्रूफ जनरल का उपयोग कर सकते हैं जिसकी एक अच्छी उपयोगिता है।

प्रूफ जनरल को स्थापित करने के लिए प्रूफ जनरल के पुराने संस्करणों को हटाकर नए वर्जन को GitHub से क्लोन किया गया

git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

फिर अपने .emacs में निम्न जोड़ें:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

सुनिश्चित करें कि आप जिस Emacs को वास्तविक Emacs चला रहे हैं। यदि आपको संस्करण बेमेल समस्याओं का सामना करना पड़ता है, तो आपको स्पष्ट रूप से Emacs पथ निर्दिष्ट करते हुए फिर से मेकफाइल चलाना पड़ सकता है

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

निक्स के साथ इंस्टालेशन

चेतावनी: यह Coq को स्थापित करने का मानक तरीका नहीं है।

लिनक्स (और मैकओएस) के उपयोगकर्ताओं के लिए जो कोक के अप-टू-डेट संस्करणों तक पहुंच प्राप्त करना चाहते हैं या एक ही मशीन पर कोक के कई संस्करणों का उपयोग करने में सक्षम हो सकते हैं, बिना ओपम का उपयोग करने की परेशानी के बिना, और इससे संकलित किए बिना। source, यह एक वैकल्पिक समाधान है।

निक्स यूनिक्स-टाइप ओएस जैसे लिनक्स और मैकओएस के लिए एक पैकेज मैनेजर है। यह अपने स्वयं के संग्रह के साथ आता है जिसे आमतौर पर डेबियन या उबंटू की तुलना में अधिक अद्यतित रखा जाता है। यह आपके वितरण के पैकेज प्रबंधक के साथ संघर्ष नहीं करता है क्योंकि यह /usr/bin और इस तरह से कुछ भी स्थापित नहीं करता है।

सबसे पहले, आपको निक्स स्थापित करने की आवश्यकता है:

$ curl https://nixos.org/nix/install | sh

यह सुनिश्चित करने के लिए कि आवश्यक पर्यावरण चर सेट हैं, या तो फिर से लॉग इन करें, या टाइप करें:

. $HOME/.nix-profile/etc/profile.d/nix.sh

फिर निम्न कमांड Coq का नवीनतम संस्करण स्थापित करेगा:

$ nix-env -iA nixpkgs.coq_8_6

आप अपने PATH में कुछ भी जोड़े बिना CoqIDE भी चला सकते हैं:

$ nix-shell -p coq_8_6 --run coqide

इसी तरह (मान लीजिए कि आपके पास पहले से ही Emacs और Proof-General इंस्टॉल हैं):

$ nix-shell -p coq_8_6 --run emacs

विभिन्न संस्करणों को चलाने के लिए यह बहुत उपयोगी है जब आपको उनकी आवश्यकता होती है। उदाहरण के लिए, Coq 8.5 को चलाने के लिए निम्नलिखित कमांड का उपयोग करें:

$ nix-shell -p coq_8_5 --run coqide

प्रेरण द्वारा प्रमाण का उदाहरण

यहाँ प्रेरण द्वारा एक सरल प्रमाण दिया गया है।

Require Import Coq.Setoids.Setoid.
Require Import Coq.Arith.Lt.

(* A number is less than or equal to itself *)
Theorem aLTEa : forall a,
    a <= a.
    auto with arith. (* This follows by simple arithmetic *)
    Qed.

Theorem simplALTE : forall a b,
    S a <= S b <-> a <= b. (* If a <= b, then a + 1 <= b + 1 *)
Proof.
Admitted.

Theorem ltAlwaysLt: forall a b,
    a <= a + b.
Proof.
  intros. (* Introduce relevant variables *)
  induction a, b. (* Induction on every variable *)
  simpl. apply aLTEa. (* 0 <= 0 + S b *)
  rewrite -> plus_O_n. auto with arith. (* 0 <= S b *)
  rewrite <- plus_n_O. apply aLTEa. (* S a <= S a + 0 *)
  rewrite <- simplALTE in IHa. (* IHa: a <= a + S b. Goal: S a <= S a + S b. *)
  apply IHa. (* We rewrote the induction hypothesis to be in the same form as the goal, so it applies immediately now *)
  Qed.