From b9382bc5f8e47e156d9cbcb3e00fc6001469aa10 Mon Sep 17 00:00:00 2001
From: nartan <bozec.tanguy@gmail.com>
Date: Thu, 12 Jan 2023 11:16:09 +0100
Subject: [PATCH] =?UTF-8?q?Resolve=20"Add=20True=20Type"=20=E2=9C=A8?=
 =?UTF-8?q?=EF=B8=8F=20Closes=20#74=20=F0=9F=90=94=EF=B8=8F=F0=9F=91=8D?=
 =?UTF-8?q?=EF=B8=8F=20Approved-by:=20belazy=20<aarthuur01@gmail.com>=20Ap?=
 =?UTF-8?q?proved-by:=20nartan=20<bozec.tanguy@gmail.com>=20Approved-by:?=
 =?UTF-8?q?=20aalbert=20<augustin.albert@bleu-azure.fr>=20Approved-by:=20v?=
 =?UTF-8?q?-lafeychine=20<vincent.lafeychine@proton.me>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

🦀️🍰🦀️🍰🦀️🍰

* fix(kernel): fix `type_true_rec`

* Apply 1 suggestion(s) to 1 file(s)

* fixed error in True recursor

* fixed the implementation of the True recursor and added the Tt type

* added true type and true recursor
---
 kernel/src/axiom/mod.rs   |  8 ++++-
 kernel/src/axiom/true_.rs | 69 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+), 1 deletion(-)
 create mode 100644 kernel/src/axiom/true_.rs

diff --git a/kernel/src/axiom/mod.rs b/kernel/src/axiom/mod.rs
index 2f604e3e..a50dbcfc 100644
--- a/kernel/src/axiom/mod.rs
+++ b/kernel/src/axiom/mod.rs
@@ -11,6 +11,7 @@ use crate::memory::term::Term;
 pub mod equality;
 pub mod false_;
 pub mod natural;
+pub mod true_;
 
 /// Enum containing all the axioms
 #[derive(Copy, Clone, Debug, Display, Eq, PartialEq, Hash)]
@@ -19,6 +20,9 @@ pub enum Axiom {
     #[display(fmt = "{_0}")]
     Equality(equality::Equality),
 
+    /// Axioms to describe True
+    True(true_::True),
+
     /// Axioms to describe False
     #[display(fmt = "{_0}")]
     False(false_::False),
@@ -33,6 +37,7 @@ impl Axiom {
     #[inline]
     pub fn add_named_axioms(arena: &mut Arena<'_>) {
         self::equality::Equality::append_to_named_axioms(arena);
+        self::true_::True::append_to_named_axioms(arena);
         self::false_::False::append_to_named_axioms(arena);
         self::natural::Natural::append_to_named_axioms(arena);
     }
@@ -40,10 +45,11 @@ impl Axiom {
     /// Get the type of a given axiom
     #[inline]
     pub fn get_type<'arena>(self, arena: &mut Arena<'arena>) -> Term<'arena> {
-        use Axiom::{Equality, False, Natural};
+        use Axiom::{Equality, False, Natural, True};
 
         match self {
             Equality(axiom) => axiom.get_type(arena),
+            True(axiom) => axiom.get_type(arena),
             False(axiom) => axiom.get_type(arena),
             Natural(axiom) => axiom.get_type(arena),
         }
diff --git a/kernel/src/axiom/true_.rs b/kernel/src/axiom/true_.rs
new file mode 100644
index 00000000..d185d46f
--- /dev/null
+++ b/kernel/src/axiom/true_.rs
@@ -0,0 +1,69 @@
+//! Set of axioms and typing rules for the `True` type
+
+use derive_more::Display;
+
+use super::{Axiom, AxiomKind};
+use crate::memory::arena::Arena;
+use crate::memory::declaration::Declaration;
+use crate::memory::level::Level;
+use crate::memory::term::Term;
+
+/// Axioms regarding `True`
+#[derive(Debug, Display, Clone, Copy, PartialEq, Eq, Hash)]
+pub enum True {
+    /// True
+    True,
+
+    /// The default inhabitant of True
+    Tt,
+
+    /// The recursor over True
+    TrueRec,
+}
+
+impl<'arena> AxiomKind<'arena> for True {
+    fn append_to_named_axioms(arena: &mut Arena<'arena>) {
+        let var0 = Level::var(0, arena);
+
+        let decl = Term::axiom(Axiom::True(Self::True), &[], arena);
+        arena.bind("True", decl);
+
+        let decl = Term::axiom(Axiom::True(Self::Tt), &[], arena);
+        arena.bind("Tt", decl);
+
+        let decl = Declaration(Term::axiom(Axiom::True(Self::TrueRec), &[var0], arena), 1);
+        arena.bind_decl("True_rec", decl);
+    }
+
+    fn get_type(self, arena: &mut Arena<'arena>) -> Term<'arena> {
+        match self {
+            Self::True => Term::sort_usize(0, arena),
+            Self::Tt => Term::axiom(Axiom::True(Self::True), &[], arena),
+            Self::TrueRec => Self::type_true_rec(arena),
+        }
+    }
+}
+
+impl True {
+    /// Type of the recursor over `False` proof witnesses
+    fn type_true_rec<'arena>(arena: &mut Arena<'arena>) -> Term<'arena> {
+        // True
+        let term_true = Term::axiom(Axiom::True(Self::True), &[], arena);
+        // Sort u
+        let sort_u = Term::sort(Level::var(0, arena), arena);
+        // True -> Sort u
+        let motive = Term::prod(term_true, sort_u, arena);
+        // motive t
+        let app_motive = Term::app(Term::var(3.into(), motive, arena), Term::var(1.into(), term_true, arena), arena);
+        // (t: True) -> motive t
+        let prod_app_motive = Term::prod(term_true, app_motive, arena);
+        // tt
+        let term_tt = Term::axiom(Axiom::True(Self::Tt), &[], arena);
+        // motive tt
+        let motive_tt = Term::app(Term::var(1.into(), motive, arena), term_tt, arena);
+        // (motive tt) -> (t: True) -> motive t
+        let prod_app_motive_tt = Term::prod(motive_tt, prod_app_motive, arena);
+        // (motive: True -> Sort u) -> (motive tt) -> (t: True) -> motive t
+        Term::prod(motive, prod_app_motive_tt, arena)
+    }
+}
-- 
GitLab