روك

برنامج Rocq Prover (المعروف سابقًا باسم Coq ) هو برنامج تفاعلي لإثبات النظريات تم إصداره لأول مرة في عام 1989. وهو يسمح بالتعبير عن التأكيدات الرياضية، والتحقق الآلي من براهين هذه التأكيدات، ويساعد في إيجاد البراهين الرسمية باستخدام إجراءات أتمتة البرهان واستخراج برنامج معتمد من البرهان البنائي لمواصفاته الرسمية .

يعتمد برنامج Rocq على نظرية حساب الإنشاءات الاستقرائية، وهي فرع من حساب الإنشاءات . لا يُعد Rocq برنامجًا آليًا لإثبات النظريات ، ولكنه يتضمن تكتيكات ( إجراءات ) آلية لإثبات النظريات ، بالإضافة إلى إجراءات اتخاذ قرارات متنوعة .

منحت جمعية آلات الحوسبة تيري كوكاند ، وجيرار هويه ، وكريستين بولين-مورينغ ، وبرونو باراس، وجان كريستوف فيلياتر، وهوجو هيربلين، وشيتان مورثي، وإيف بيرتو، وبيير كاستيران جائزة نظام البرمجيات لعام 2013 عن برنامج روك (عندما كان يُطلق عليه اسم كوك).

عند النظر إلى Rocq كلغة برمجة ، فإنها تُطبّق نموذج برمجة وظيفية مُعتمدة على النوع ؛ ^{[ 2 ]} وعند النظر إليها كنظام منطقي، فإنها تُطبّق نظرية أنواع من الرتبة العليا . وقد حظي تطوير Rocq بدعم المعهد الفرنسي لأبحاث علوم الحاسوب والأتمتة (INRIA) منذ عام 1984، بالتعاون مع العديد من المؤسسات البحثية الفرنسية والدولية الأخرى. بدأ تطوير Rocq على يد جيرار هويه وتيري كوكاند، وساهم أكثر من 200 شخص، ^{[ 3 ]} معظمهم من الباحثين، في تطوير ميزات النظام الأساسي منذ إنشائه. وتولى تنسيق فريق التنفيذ تباعًا كل من جيرار هويه، وكريستين بولان-مورينغ، وهوغو هيربلين، وماثيو سوزو. تُطبّق Rocq بشكل أساسي بلغة OCaml مع بعض لغة C. ويمكن توسيع النظام الأساسي من خلال آلية الإضافات . ^{[ 4 ]}

توفر Rocq لغة مواصفات تُسمى Gallina. ^{[ 5 ]} تتميز البرامج المكتوبة بلغة Gallina بخاصية التطبيع الضعيف ، مما يعني أنها تنتهي دائمًا. تُعد هذه خاصية مميزة للغة، حيث أن الحلقات اللانهائية (البرامج غير المنتهية) شائعة في لغات البرمجة الأخرى. ^{[ 6 ]}

كمثال على برهان مكتوب بلغة روك، لننظر في برهان لِمّة تنص على أن أخذ العدد التالي لعدد طبيعي يقلب زوجيته. تُستخدم تكتيكة الطي والفك التي قدمها دانفي ^{[ 7 ]} لتبسيط البرهان.

من مكتبة Stdlib Require استيراد Arith Nat Bool .Fixpoint is_even ( n : nat ) : bool := match n with | 0 => true | S n' => negb ( is_even n' ) end .اللمة is_even_0 : is_even 0 = صحيح . البرهان . الانعكاسية . انتهى البرهان .اللمة is_even_S n : is_even ( S n ) = negb ( is_even n ). البرهان . الانعكاسية . انتهى البرهان .اللمة: successor_flips_evenness n : is_even n = negb ( is_even ( S n )). البرهان : إعادة كتابة is_even_S . destruct ( is_even n ). * simpl . reflexivity . * simpl . reflexivity . Qed .

يبدأ هذا البرهان باستيراد تعريفات القيم المنطقية والأعداد الطبيعية من المكتبة القياسية، ثم يُعرّف is_evenدالة تُحدد ما إذا كان العدد زوجيًا أم لا. بعد ذلك، يتم إثبات ثلاث لمات حول هذه الدالة. تُعيد الأولى صياغة المعادلات التعريفية للدالة is_even، وبما أن روك يعرف هذه المعادلات، فإن برهانه قصير جدًا. أما اللمة الأخيرة، فتُثبت بتمييز الحالات بعد تطبيق اللمة الثانية أولًا؛ *وتشير النجمة إلى بداية حالة فرعية جديدة.

• CompCert : مُترجم مُحسِّن لجميع لغات البرمجة C تقريبًا ، والذي تمت برمجته وإثبات صحته إلى حد كبير في Rocq.
• تم نشر برهان صحة بنية البيانات المنفصلة في Rocq في عام 2007. ^{[ 11 ]}
• تم الانتهاء من البرهان الرسمي لنظرية فيت-تومسون باستخدام برنامج روك في سبتمبر 2012. ^{[ 12 ]}
• القندس النشيط : تم اكتشاف قيمة القندس النشيط الفائز في الولايات الخمس بواسطة هاينر ماركسن ويورغن بونتروك في عام 1989، ولكن لم يثبت أنه القندس النشيط الخامس الفائز - الذي يُرمز له بـ BB(5) - إلا في عام 2024 باستخدام برهان في روك. ^{[ 13 ] [ 14 ]}

بالإضافة إلى بناء مصطلحات غالينا بشكل صريح، يدعم برنامج روك استخدام التكتيكات المكتوبة بلغة Ltac المدمجة أو بلغة OCaml. تعمل هذه التكتيكات على أتمتة بناء البراهين، من خلال تنفيذ الخطوات البسيطة أو البديهية فيها. ^{[ 15 ]} تُنفذ العديد من التكتيكات إجراءات اتخاذ القرار لنظريات مختلفة. على سبيل المثال، يُحدد تكتيك "الحلقة" نظرية المساواة modulo بديهيات الحلقة أو شبه الحلقة عبر إعادة الكتابة الترابطية - التبديلية . ^{[ 16 ]} على سبيل المثال، يُثبت البرهان التالي مساواة معقدة في حلقة الأعداد الصحيحة في سطر واحد فقط من البرهان: ^{[ 17 ]}

Require Import ZArith . Open Scope Z_scope . Goal forall a b c : Z , ( a + b + c ) ^ 2 = a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c . intros ; ring . Qed .

تتوفر أيضًا إجراءات قرار مدمجة للنظرية الفارغة ("التطابق")، والمنطق الافتراضي ("التلقائي")، والحساب الخطي للأعداد الصحيحة الخالي من المُكمِّمات ("الحساب الخطي للأعداد الصحيحة")، والحساب الخطي للأعداد النسبية/الحقيقية ("الحساب الخطي للأعداد الحقيقية"). ^{[ 18 ] [ 19 ]} وقد طُوِّرت إجراءات قرار إضافية كمكتبات، بما في ذلك مكتبة لجبر كلين ^{[ 20 ]} ومكتبة أخرى لأهداف هندسية محددة . ^{[ 21 ]}

The old name Coq means 'rooster' in French and is a wordplay on the name of Thierry Coquand, calculus of constructions or CoC, and stems from a French tradition of naming research development tools after animals.^[22] Until 1991, Coquand was implementing a language named the calculus of constructions and it was simply called CoC then. In 1991, a new implementation based on the extended calculus of inductive constructions was begun and the name changed from CoC to Coq in an indirect reference to Coquand, who developed the calculus of constructions along with Gérard Huet and contributed to the calculus of inductive constructions with Christine Paulin-Mohring.^[23] On October 11, 2023, the development team announced that Coq would be renamed The Rocq Prover in coming months, and began updating the code base, website, and related tools.^[24] The official renaming happened with the release of Rocq 9.0 in March 2025.^[25] The new name refers to Inria Rocquencourt, where the system was developed first, and is related to the mythical bird Roc, which allows keeping the bird references from the prior name.^[26]

• 2022 Open Science Award for Open Source Research Software in the category "Scientific and Technical" ^[27]

• Calculus of constructions
• Curry–Howard correspondence
• Intuitionistic type theory
• List of proof assistants

• الموقع الرسمي