Work on sko_forall

carcara/lambdapi/Alethe.lp

@@ -422,20 +422,98 @@ begin
   }
 end;
 
+opaque symbol imp_eq_or p q: πᶜ (((¬ p) ∨ᶜ q) =  (p ⇒ᶜ q)) ≔
+begin
+  assume p q;
+  apply prop_ext;
+  apply ∧ᶜᵢ
+  { apply ⇒ᶜᵢ; assume Hor; apply or_to_imply Hor }
+  { apply ⇒ᶜᵢ; assume Himp; apply imply_to_or Himp }
+end;
+
+opaque symbol contrapos [p q] : πᶜ (p ⇒ᶜ q  ⇔ᶜ (¬ q ⇒ᶜ ¬ p)) ≔
+begin
+  assume p q;
+  apply ∧ᶜᵢ
+  {
+    apply ⇒ᶜᵢ;
+    assume Himp;
+    apply ⇒ᶜᵢ;
+    assume Hnq;
+    apply ¬ᶜᵢ;
+    assume Hp;
+    have Hq: πᶜ q
+    {  apply ⇒ᶜₑ Himp Hp };
+    apply ¬ᶜₑ Hnq Hq
+  }
+  {
+    apply ⇒ᶜᵢ;
+    assume Himp;
+    apply ⇒ᶜᵢ;
+    assume Hp;
+    have Hor: πᶜ ((¬ ¬ q) ∨ᶜ ¬ p) {
+      rewrite imp_eq_or;
+      apply Himp
+    };
+    apply ∨ᶜₑ Hor
+    { assume Hnnq; rewrite left  nnpp_eq; apply Hnnq }
+    { assume Hnp; apply  ¬ᶜₑ Hnp Hp }
+  };
+end;
+
+opaque symbol contradiction p : (πᶜ (¬ p) → πᶜ ⊥) → πᶜ p ≔
+begin
+  assume p Hnp;
+  admit
+end;
 
 // // Hilbert epsilon operator/choice
-constant symbol ϵ  [a]: (τ a → Prop) → τ a; notation ϵ quantifier;
+symbol ϵ  [a]: (τ a → Prop) → τ a; notation ϵ quantifier;
 
-constant symbol ϵᵢ x p : πᶜ (p x) → πᶜ (p (ϵ p));
+constant symbol ϵᵢ [a] x (p: τ a → Prop) : πᶜ (p x) → πᶜ (p (ϵ p));
 constant symbol ϵ_det [p q]: Π x, πᶜ ((p x) ⇔ᶜ (q x)) → πᶜ (ϵ p = ϵ q);
 
-opaque symbol imp_eq_or p q: πᶜ (((¬ p) ∨ᶜ q) =  (p ⇒ᶜ q)) ≔
+opaque symbol ϵ_to_∃ [a] p: πᶜ ((`∃ᶜ (x : τ a),  p x) = p (`ϵ (x : τ a), p x)) ≔
 begin
-  assume p q;
+  assume a p;
   apply prop_ext;
   apply ∧ᶜᵢ
-  { apply ⇒ᶜᵢ; assume Hor; apply or_to_imply Hor }
-  { apply ⇒ᶜᵢ; assume Himp; apply imply_to_or Himp }
+  {
+    apply ⇒ᶜᵢ;
+    assume H;
+    apply ∃ᶜₑ _ H;
+    assume x H1;
+    apply ϵᵢ x (λ u, (p u)) H1;
+  }
+  {
+    apply ⇒ᶜₑ (∧ᶜₑ₂ (@contrapos (p (`ϵ x, p x) ) (`∃ᶜ x, p x)));
+    apply ⇒ᶜᵢ;
+    assume H;
+    have H1: πᶜ (`∀ᶜ x, ¬ p x) { apply (⇒ᶜₑ (∧ᶜₑ₁ (nex_forall p)) H) };
+    admit
+    //type ∀ᶜₑ (λ u, ¬ (p u)) H1
+  }
+end;
+
+opaque symbol ϵ_to_∀ [a] p: πᶜ ((`∀ᶜ (x : τ a), p x) = p (`ϵ (x : τ a), (¬ p x))) ≔
+begin
+  assume a p;
+  apply prop_ext;
+  apply ∧ᶜᵢ
+  {
+    apply ⇒ᶜᵢ;
+    assume H;
+    apply ∀ᶜₑ (`ϵ x, ¬ (p x)) H
+  }
+  {
+    apply ⇒ᶜₑ (∧ᶜₑ₂ (@contrapos (p (`ϵ x, ¬ (p x)) ) (`∀ᶜ x, p x)));
+    apply ⇒ᶜᵢ;
+    assume H;
+    have H1: πᶜ (`∃ᶜ x, ¬ p x) { refine (⇒ᶜₑ (∧ᶜₑ₁ (nforall_ex p)) H) };
+    apply ∃ᶜₑ _ H1;
+    assume x Hnpx;
+    apply ϵᵢ x (λ u, ¬ (p u)) Hnpx;
+  }
 end;
 
 opaque  symbol and_identity_r x : πᶜ ((x ∧ᶜ ⊤) = x) ≔
@@ -1391,6 +1469,56 @@ begin
   };
 end;
 
+opaque symbol bind_∀' [a p q]: (Π (x: τ a), Π (y: τ a), πᶜ (x = y) → πᶜ (p x = q y))  → πᶜ ((`∀ᶜ (x: τ a), p x) = (`∀ᶜ (y: τ a), q y)) ≔
+begin
+  assume a p q;
+  assume H;
+  apply prop_ext;
+  apply ∧ᶜᵢ 
+  {
+    apply ⇒ᶜᵢ;
+    assume H1;
+    apply ∀ᶜᵢ _;
+    assume x;
+    have Hpx: πᶜ (p x) { apply ∀ᶜₑ x H1; };
+    rewrite left H x x (eq_reflᶜ x);
+    apply Hpx
+  }
+  {
+    apply ⇒ᶜᵢ;
+    assume H1;
+    apply ∀ᶜᵢ _;
+    assume x;
+    have Hqx: πᶜ (q x) { apply ∀ᶜₑ x H1 };
+    rewrite H x x (eq_reflᶜ x);
+    apply Hqx;
+  };
+end;
+
+opaque symbol sko_forall [a p q]: (Π (x: τ a), πᶜ (x = `ϵ (y: τ a), ¬ (p y)) → πᶜ (p x = q))  → πᶜ ((`∀ᶜ (x: τ a), p x) = q) ≔
+begin
+  assume a p q H;
+  apply prop_ext;
+  apply ∧ᶜᵢ
+  {
+    apply ⇒ᶜₑ (∧ᶜₑ₂ (@contrapos (`∀ᶜ x, p x) q));
+    apply ⇒ᶜᵢ;
+    assume Hnq;
+    rewrite .[x in ¬ x]  (ϵ_to_∀ p);
+    have H1:  πᶜ (p (`ϵ x, ¬ (p x)) = q) { apply H; reflexivity };
+    rewrite H1;
+    apply Hnq
+  }
+  {
+    rewrite .[x in _ ⇒ᶜ x]  (ϵ_to_∀ p);
+    apply ⇒ᶜᵢ;
+    assume Hq;
+    have H1:  πᶜ (p (`ϵ y, ¬ (p y)) = q) { apply H; reflexivity };
+    rewrite H1;
+    apply Hq
+  }
+end;
+
 require open Stdlib.Nat;
 
 // Inductive t A : nat -> Type :=
@@ -1405,7 +1533,7 @@ rule τ (vec $a $n) ↪ Vec $a $n;
 
 symbol distinct a n : Vec a n → Prop; 
 
-type (cons 2 a (cons 1 b (cons 0 c □)));
+//type (cons 2 a (cons 1 b (cons 0 c □)));
 
 // boolean case
 rule distinct o _ □ ↪ ⊤
@@ -1445,4 +1573,4 @@ opaque symbol feq3ᶜ [a b c d] (f:τ a → τ b →  τ c → τ d):
   Π [x x':τ a], πᶜ(x = x') → Π [y y':τ b], πᶜ(y = y') → Π [z z':τ c], πᶜ(z = z') → πᶜ(f x y z = f x' y' z') ≔
 begin
   assume a b c d f x x' xx' y y' yy' z z' zz'; rewrite xx'; rewrite yy'; rewrite zz'; reflexivity
-end;
+end;

carcara/lambdapi/Classic.lp

@@ -422,3 +422,7 @@ begin
     { apply ⇒ᶜᵢ; assume hp; refine ⇒ᶜₑ (∧ᶜₑ₁ eqr) (⇒ᶜₑ (∧ᶜₑ₁ epq) hp) }
     { apply ⇒ᶜᵢ; assume hr; refine ⇒ᶜₑ (∧ᶜₑ₂ epq) (⇒ᶜₑ (∧ᶜₑ₂ eqr) hr) }
 end;
+
+opaque symbol nforall_ex [a] p : πᶜ ((¬ (`∀ᶜ (x : τ a), p x)) ⇔ᶜ (`∃ᶜ (x : τ a), ¬ p x)) ≔ begin admit end;
+
+opaque symbol nex_forall [a] p : πᶜ ((¬ (`∃ᶜ (x : τ a), p x)) ⇔ᶜ (`∀ᶜ (x : τ a), ¬ p x)) ≔ begin admit end;

carcara/src/lambdapi/mod.rs

@@ -5,7 +5,7 @@ use crate::ast::{
 };
 use crate::parser::FunctionDef;
 use indexmap::IndexMap;
-use std::collections::VecDeque;
+use std::collections::{HashMap, VecDeque};
 use std::fmt::{self};
 use std::ops::Deref;
 use std::time::Duration;
@@ -175,15 +175,15 @@ macro_rules! tactic {
         $steps.push(ProofStep::Try(Box::new(step)));
         tactic![ $steps, $(  $body )* ]
     };
-    ($steps:ident, rewrite [$($i:tt)+] $( ( $($args:tt) + ) ) *  $($body:tt)+) => {
+    ($steps:ident, rewrite [$($i:tt)+] $( ( $($args:tt) + ) ) * ; $($body:tt)+) => {
         $steps.push(ProofStep::Rewrite(None, $($i)+, vec![ $( make_term![  $( $args )+ ] , )* ]));
         tactic![ $steps, $( $body )+ ]
     };
-    ($steps:ident, rewrite .$pattern:tt $i:tt  $( ( $($args:tt) + ) ) *  $($body:tt)+) => {
+    ($steps:ident, rewrite .$pattern:tt $i:tt  $( ( $($args:tt) + ) ) * ; $($body:tt)+) => {
         $steps.push(ProofStep::Rewrite(Some($pattern.to_string()), Term::from($i), vec![ $( make_term![  $( $args )+ ] , )* ]));
         tactic![ $steps, $( $body )+ ]
     };
-    ($steps:ident, rewrite $i:tt  $( ( $($args:tt) + ) ) *  $($body:tt)+) => {
+    ($steps:ident, rewrite $i:tt  $( ( $($args:tt) + ) ) * ; $($body:tt)+) => {
         $steps.push(ProofStep::Rewrite(None, Term::from($i), vec![ $( make_term![  $( $args )+ ] , )* ]));
         tactic![ $steps, $( $body )+ ]
     };
@@ -673,23 +673,35 @@ fn translate_subproof<'a>(
 ) -> TradResult<Vec<ProofStep>> {
     let subproof = commands.last().unwrap();
 
+    //Get the last step of the proof
     let (id, clause, rule) = unwrap_match!(
         subproof,
         ProofCommand::Step(AstProofStep { id, clause, rule,.. }) => (normalize_name(id), clause, rule)
     );
 
-    let assignment_args = assignment_args
-        .into_iter()
-        .map(|(_, term)| Term::from(term))
-        .collect_vec();
-
     let clause = clause.iter().map(From::from).collect_vec();
 
     let mut fresh_ctx = Context::default();
     fresh_ctx.sharing_map = context.sharing_map.clone();
 
     let mut proof_cmds = translate_commands(&mut fresh_ctx, iter)?;
 
+    proof_cmds
+        .iter_mut()
+        .filter(|cmd| matches!(cmd, ProofStep::Have(_, _, _)))
+        .for_each(|cmd| match cmd {
+            ProofStep::Have(name, cl, steps) => {
+                cl.visit(assignment_args);
+                *cmd = ProofStep::Have(name.to_string(), cl.clone(), steps.to_vec());
+            },
+            _ => {},
+        } );
+
+    let assignment_args = assignment_args
+        .into_iter()
+        .map(|(_, term)| Term::from(term))
+        .collect_vec();
+
     //TODO: Remove this side effect by append the prelude in translate_commands and return the  pair Subproof + Axioms in subproof
     context.prelude.append(&mut fresh_ctx.prelude); // Add subproof of current subproof to the prelude
 
@@ -744,6 +756,20 @@ fn translate_subproof<'a>(
             Term::Alethe(LTerm::Proof(Box::new(Term::Alethe(LTerm::Clauses(clause))))),
             proof,
         )
+    } else if rule == "sko_forall" {
+        let last_step_id = unwrap_match!(commands.get(commands.len() - 1), Some(ProofCommand::Step(AstProofStep{id, ..})) => normalize_name(id));
+
+        // end of the script
+        proof_cmds.append(&mut lambdapi! {
+            apply "∨ᶜᵢ₁";
+            apply "π̇ₗ" (@last_step_id.into());
+        });
+
+        ProofStep::Have(
+            id.to_string(),
+            Term::Alethe(LTerm::Proof(Box::new(Term::Alethe(LTerm::Clauses(clause))))),
+            proof_cmds,
+        )
     } else {
         let psy_id = unwrap_match!(commands.get(commands.len() - 2), Some(ProofCommand::Step(AstProofStep{id, ..})) => normalize_name(id));
 
@@ -866,8 +892,12 @@ fn translate_tautology(
 
     let steps = match rule {
         "bind" | "subproof" => None,
+        "false" => Some(translate_false()),
         "forall_inst" => Some(translate_forall_inst(args)),
-        "cong" => Some(translate_cong(clause, premises.as_slice())),
+        "cong" => {
+            /* println!("{}", id) ; */
+            Some(translate_cong(clause, premises.as_slice()))
+        }
         "and_neg" | "or_neg" | "and_pos" | "or_pos" => Some(translate_auto_rewrite(rule)),
         "not_or" => Some(translate_not_or(premises.first()?)),
         "implies" => Some(translate_implies(premises.first()?.0.as_str())),
@@ -879,7 +909,8 @@ fn translate_tautology(
         "refl" => Some(translate_refl()),
         "and" => Some(translate_and(premises.first()?)),
         "or" => Some(translate_or(premises.first()?.0.as_str())),
-        "hole" | "reordering" | "contraction" => Some(Ok(Proof(vec![ProofStep::Admit]))), // Rule specific to Carcara
+        "sko_forall" => Some(translate_sko_forall()),
+        "hole" | "reordering" | "contraction" => Some(Ok(Proof(vec![ProofStep::Admit]))), // specific rules of CVC5
         _ => Some(translate_simple_tautology(rule, premises.as_slice())),
     };
 

carcara/src/lambdapi/printer.rs

@@ -303,7 +303,7 @@ impl PrettyPrint for LTerm {
                 => COMMA
                 => space()
                 => p.to_doc()
-            ),
+            ).parens(),
         }
     }
 }