Skip to content

Commit

Permalink
Fix forall_inst and make subproof rule use symbols
Browse files Browse the repository at this point in the history
  • Loading branch information
@NotBad4U
NotBad4U committed Oct 30, 2024
1 parent 33c7832 commit 634cc77
Show file tree
Hide file tree
Showing 5 changed files with 203 additions and 75 deletions.
76 changes: 49 additions & 27 deletions carcara/src/lambdapi/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -652,30 +652,17 @@ fn translate_subproof<'a>(
} else if rule == "sko_forall" {
let last_step_id = unwrap_match!(commands.get(commands.len() - 1), Some(ProofCommand::Step(AstProofStep{id, ..})) => normalize_name(id));

//FIXME: hahah
// end of the script
proof_cmds.append(&mut lambdapi! {
apply "∨ᶜᵢ₁";
apply "π̇ₗ" (@last_step_id.into());
});

proof_cmds
// proof_cmds.append(&mut lambdapi! {
// apply "∨ᶜᵢ₁";
// apply "π̇ₗ" (@last_step_id.into());
// });
// proof_cmds.push(ProofStep::Admit);

// proof_cmds
admit()
} else {
let psy_id = unwrap_match!(commands.get(commands.len() - 2), Some(ProofCommand::Step(AstProofStep{id, ..})) => normalize_name(id));

let discharge = unwrap_match!(commands.last(), Some(ProofCommand::Step(AstProofStep{id: _, clause:_, rule:_, premises:_, args:_, discharge})) => discharge);

let premises_discharge = get_premises_clause(iter, discharge);

let subproof_tactic = Term::TermId(format!("subproof{}", premises_discharge.len()));

let mut args = premises_discharge
.into_iter()
.map(|(id, _)| unary_clause_to_prf(id.as_str()))
.collect_vec();
args.push(unary_clause_to_prf(psy_id.as_str()));

proof_cmds.push(ProofStep::Apply(subproof_tactic, args, SubProofs(None)));

proof_cmds
};

Expand Down Expand Up @@ -923,6 +910,14 @@ where
depth + 1,
)?;

let sub = commands.last().unwrap();

//Get the last step of the proof
let (_, _, rule) = unwrap_match!(
sub,
ProofCommand::Step(AstProofStep { id, clause, rule,.. }) => (normalize_name(id), clause, rule)
);

ctx.deps
.insert(normalize_name(&id), (ctx.index, depth, HashSet::new()));

Expand Down Expand Up @@ -950,11 +945,38 @@ where
.and_modify(|(_, _, ds)| ds.extend(deps_subproof.iter()));
}

proof_steps.push(f(
normalize_name(id),
Term::Alethe(LTerm::Proof(Box::new(Term::Alethe(LTerm::Clauses(clause))))),
Some(subproof),
));
if rule.contains("subproof") {
let res = subproof.into_iter().map(|s| unwrap_match!(s, ProofStep::Have(id, r#type, proof) => f(id, r#type, Some(proof)))).collect_vec();
proof_steps.extend(res);

let psy_id = unwrap_match!(commands.get(commands.len() - 2), Some(ProofCommand::Step(AstProofStep{id, ..})) => normalize_name(id));

let discharge = unwrap_match!(commands.last(), Some(ProofCommand::Step(AstProofStep{id: _, clause:_, rule:_, premises:_, args:_, discharge})) => discharge);

let premises_discharge = get_premises_clause(proof_iter, discharge);

let subproof_tactic = Term::TermId(format!("subproof{}", premises_discharge.len()));

let mut args = premises_discharge
.into_iter()
.map(|(id, _)| unary_clause_to_prf(id.as_str()))
.collect_vec();
args.push(unary_clause_to_prf(psy_id.as_str()));

//proof_cmds.push(ProofStep::Apply(subproof_tactic, args, SubProofs(None)));

proof_steps.push(f(
normalize_name(id),
Term::Alethe(LTerm::Proof(Box::new(Term::Alethe(LTerm::Clauses(clause))))),
Some(vec![ProofStep::Apply(subproof_tactic, args, SubProofs(None))]),
));
} else {
proof_steps.push(f(
normalize_name(id),
Term::Alethe(LTerm::Proof(Box::new(Term::Alethe(LTerm::Clauses(clause))))),
Some(subproof),
));
}
}
};
ctx.index += 1;
Expand Down
19 changes: 16 additions & 3 deletions carcara/src/lambdapi/proof.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,17 +39,30 @@ pub enum ProofStep {
Simplify,
}


macro_rules! assume {
($id:ident) => {
ProofStep::Assume(vec![ stringify!($id).to_string() ])
}
}

pub(crate) use assume;


macro_rules! apply {
($id:ident) => {
ProofStep::Apply(Term::TermId(stringify!($id).into()), vec![], SubProofs(None))
};
($t:expr) => {
ProofStep::Apply($t, vec![], SubProofs(None))
};
($id:expr, [ $($sp:expr),+ $(,)? ]) => {
ProofStep::Apply(Term::TermId(stringify!($id).into()), vec![], SubProofs(Some(
($t:expr, { $($arg:expr),+ $(,)? }) => {
ProofStep::Apply($t, vec![$($arg),+], SubProofs(None))
};
($id:expr, { $($arg:expr),* $(,)? }, [ $($sp:expr),* $(,)? ]) => {
ProofStep::Apply(Term::TermId(stringify!($id).into()), vec![$($arg),*], SubProofs(Some(
vec![
$( proof!($sp)),+
$( proof!($sp) ),*
]
)))
};
Expand Down
158 changes: 122 additions & 36 deletions carcara/src/lambdapi/tautology.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -352,32 +352,51 @@ pub fn translate_simple_tautology(
)]))
}

pub fn translate_forall_inst(_args: &Vec<Rc<AletheTerm>>) -> TradResult<Proof> {
Ok(Proof(admit()))
// let hyp = Term::from("H");

// // The term Term::from("H") is related to assume [H];
// let init_forall_elim = Term::Terms(vec![
// Term::from("∀ᶜₑ"),
// unwrap_match!(args.first(), Some(ProofArg::Assign(_, t)) => t.into()),
// hyp,
// ]);

// let forall_elims = args.into_iter().skip(1).fold(init_forall_elim, |acc, arg| {
// Term::Terms(vec![
// Term::from("∀ᶜₑ"),
// unwrap_match!(arg, ProofArg::Assign(_, t) => t.into()),
// acc,
// ])
// });
/// Construct the proof term to validate forall_inst rule.
/// Considering the example below:
/// ```text
/// (step tᵢ (cl (or (not (forall ((x S) (y T)) (P y x )))
/// (P b (f a))
/// :rule forall_inst :args ((f a) b)
/// ```
///
/// We will translate `forall_inst` changing the or (not a) b into an implication.
/// Passing the left handside into the hypothesis and then applying
/// n-|args| times forall eliminator.
///
/// NOTE: The convertion of arguments do not use the context for sharing the symbol for now.
///
/// Thus, the example is translated into the proof script:
/// ```text
/// have tᵢ: (((¬ (`∀ᶜ ((x: τ S) (y: τ T)) (P y x ))) ∨ᶜ (P b (f a))) ⟇ ▩) {
/// apply ∨ᶜᵢ₁;
/// apply imply_to_or;
/// apply ⇒ᶜᵢ;
/// assume H;
/// apply ∀ᶜₑ b (∀ᶜₑ (f a) H)
/// }
/// ```
pub fn translate_forall_inst(args: &Vec<Rc<AletheTerm>>) -> TradResult<Proof> {
//Ok(Proof(admit()))
let hyp = Term::from("H");

let init_forall_elim = Term::Terms(vec![
Term::from("∀ᶜₑ"),
args.first().expect("empty args").into(),
hyp,
]);

// Ok(Proof(lambdapi! {
// apply "∨ᶜᵢ₁";
// apply "imply_to_or";
// apply "⇒ᶜᵢ";
// assume [H]; //FIXME: use hyp instead
// apply "" (@forall_elims);
// }))
let forall_elims = args.into_iter().skip(1).fold(init_forall_elim, |acc, arg| {
Term::Terms(vec![Term::from("∀ᶜₑ"), arg.into(), acc])
});

Ok(Proof(lambdapi! {
apply "∨ᶜᵢ₁";
apply "imply_to_or";
apply "⇒ᶜᵢ";
assume [H]; //FIXME: use hyp instead
apply "" (@forall_elims);
}))
}

pub fn translate_sko_forall() -> TradResult<Proof> {
Expand All @@ -393,7 +412,10 @@ pub fn translate_sko_forall() -> TradResult<Proof> {
#[cfg(test)]
mod tests_tautolog {
use super::*;
use crate::parser::{self, parse_instance};
use crate::{
ast::BindingList,
parser::{self, parse_instance},
};

#[test]
fn test_transitivity_translation() {
Expand Down Expand Up @@ -492,11 +514,13 @@ mod tests_tautolog {
)),
Some(proof!(apply!(
cong_or,
{},
[
apply!(h1),
apply!(
cong_or,
[apply!(h2), apply!(cong_or, [apply!(h3), apply!(h4)]),]
{},
[apply!(h2), apply!(cong_or, {}, [apply!(h3), apply!(h4)]),]
)
]
))),
Expand Down Expand Up @@ -552,11 +576,13 @@ mod tests_tautolog {
)),
Some(proof!(apply!(
cong_and,
{},
[
apply!(h1),
apply!(
cong_and,
[apply!(h2), apply!(cong_and, [apply!(h3), apply!(h4)]),]
{},
[apply!(h2), apply!(cong_and, {}, [apply!(h3), apply!(h4)]),]
)
]
))),
Expand Down Expand Up @@ -597,13 +623,12 @@ mod tests_tautolog {
None,
"t3".into(),
vec![],
cl!(eq!(Box::new(not!(id!("a"))), Box::new(not!(id!("b"))))),
cl!(eq!(not!(id!("a")), not!(id!("b")))),
Some(proof!(
apply!(id!("∨ᶜᵢ₁")),
ProofStep::Apply(
apply!(
id!("feqᶜ"),
vec![id!("(¬)"), unary_clause_to_prf("h1")],
SubProofs(None)
{ id!("(¬)"), unary_clause_to_prf("h1") }
)
)),
);
Expand Down Expand Up @@ -646,10 +671,7 @@ mod tests_tautolog {
None,
"t3".into(),
vec![],
cl!(eq!(
Box::new(imp!(id!("a"), id!("b"))),
Box::new(imp!(id!("c"), id!("d")))
)),
cl!(eq!(imp!(id!("a"), id!("b")), imp!(id!("c"), id!("d")))),
Some(proof!(
apply!(id!("∨ᶜᵢ₁")),
apply!(terms![
Expand All @@ -663,4 +685,68 @@ mod tests_tautolog {

assert_eq!(t3, cmd);
}

#[test]
fn test_forall_inst_translation() {
let problem: &[u8] = b"
(declare-sort S 0)
(declare-sort T 0)
(declare-fun a () S)
(declare-fun b () T)
(declare-fun f (S) S)
(declare-fun P (T S) Bool)
";
let proof = b"
(step t1 (cl (or (not (forall ((x S) (y T)) (P y x ))) (P b (f a)))) :rule forall_inst :args ((f a) b))
";
let (_, proof, _) = parse_instance(problem, proof, parser::Config::new()).unwrap();

assert_eq!(1, proof.commands.len());

let res = translate_commands(
&mut Context::default(),
&mut proof.iter(),
0,
|id, t, ps| {
Command::Symbol(None, normalize_name(id), vec![], t, ps.map(|ps| Proof(ps)))
},
)
.expect("translate forall_inst");

assert_eq!(1, res.len());

let t1 = res.last().unwrap().clone();

let cmd_expected = Command::Symbol(
None,
"t1".into(),
vec![],
cl!(or!(
not!(forall!(
[(id!("x"), tau("S".into())), (id!("y"), tau("T".into()))],
Term::Terms(vec![id!("P"), id!("y"), id!("x")])
)),
Term::Terms(vec![
id!("P"),
id!("b"),
Term::Terms(vec![id!("f"), id!("a")])
])
)),
Some(proof!(
apply!(id!("∨ᶜᵢ₁")),
apply!(id!("imply_to_or")),
apply!(id!("⇒ᶜᵢ")),
assume!(H),
apply!(id!(""), {
terms!(
id!("∀ᶜₑ"),
id!("b"),
terms!(id!("∀ᶜₑ"), terms!(id!("f"), id!("a")), id!("H")),
)
})
)),
);

assert_eq!(t1, cmd_expected);
}
}
Loading

0 comments on commit 634cc77

Please sign in to comment.