Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Lra #54

Merged
merged 11 commits into from
Nov 22, 2022
Prev Previous commit
Next Next commit
Handle non Prop goals in lra
  • Loading branch information
proux01 authored and pi8027 committed Nov 22, 2022
commit a90013e3b45c263f6227ee9cdc8d6eba371ab8e3
4 changes: 2 additions & 2 deletions examples/lra_examples.v
Original file line number Diff line number Diff line change
@@ -101,8 +101,8 @@ Qed.

Lemma test_exfalso x (xle2 : x <= 2%:R) (xge3 : x >= 3%:R) : bool.
Proof.
(* lra. *)
Abort.
lra.
Qed.

Lemma test_rat_constant x : 0 <= x -> 1 / 3 * x <= 2^-1 * x.
Proof.
21 changes: 15 additions & 6 deletions theories/lra.elpi
Original file line number Diff line number Diff line change
@@ -285,21 +285,30 @@ quote.hyps F [def _ _ _ _|Ctx] Type TypeF Type' TypeF' VM :- !,
quote.hyps F Ctx Type TypeF Type' TypeF' VM.
quote.hyps _ [] Type TypeF Type TypeF _.

% [exfalso_if_not_prop In Out Bool] changes [In] to [False]
% when [In] is not a [Prop] (and then set [Bool] to [true])
pred exfalso_if_not_prop i:term, o:term, o:term.
exfalso_if_not_prop Type Type {{ false }} :-
coq.typecheck Type {{ Prop }} ok.
exfalso_if_not_prop _ {{ False }} {{ true }}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Main tactic

% This calls the Ltac1 tactic "lraF" with the following arguments:
% - [Type'] a term of type [Prop], an implication with the goal
% - [Efalso] a term of type [bool] indicating if the goal was changed to [False]
% - [Type''] a term of type [Prop], an implication with the goal
% and selected hypotheses
% - [TypeF'] the reified [Type'] as a [BFormula (Formula Q) Tauto.isProp]
% - [TypeF'] the reified [Type''] as a [BFormula (Formula Q) Tauto.isProp]
% - [VM''] a variable map, giving the interpretation to variables in [TypeF']
% it is of type [VarMap.t F] where [F] is the carrier for the detected
% [realFieldType]
solve (goal Ctx _Trigger Type _Proof _Args as G) GL :-
exfalso_if_not_prop Type Type' Efalso,
std.rev Ctx Ctx', !,
fstr Ctx' Type F, !,
quote F Type TypeF VM, !,
quote.hyps F Ctx' Type TypeF Type' TypeF' VM, !,
fstr Ctx' Type' F, !,
quote F Type' TypeF VM, !,
quote.hyps F Ctx' Type' TypeF Type'' TypeF' VM, !,
std.assert-ok!
(coq.typecheck TypeF' {{ BFormula (Formula Q) isProp }})
"The reification produced an ill-typed result, this is a bug.",
@@ -308,5 +317,5 @@ solve (goal Ctx _Trigger Type _Proof _Args as G) GL :-
{{ Internals.vm_of_list lp:VM' }}
{{ VarMap.t lp:FS }}
VM'',
(coq.ltac.call "lraF" [trm Type', trm TypeF', trm VM''] G GL;
(coq.ltac.call "lraF" [trm Efalso, trm Type'', trm TypeF', trm VM''] G GL;
coq.ltac.fail 0).
3 changes: 2 additions & 1 deletion theories/lra.v
Original file line number Diff line number Diff line change
@@ -241,7 +241,8 @@ Definition vm_of_list T (l : list T) : VarMap.t T :=
End Internals.

(* Main tactic, called from the elpi parser (c.f., lra.elpi) *)
Ltac lraF hyps_goal ff varmap :=
Ltac lraF efalso hyps_goal ff varmap :=
match efalso with true => exfalso | _ => idtac end;
(suff: hyps_goal by exact);
pi8027 marked this conversation as resolved.
Show resolved Hide resolved
let iff := fresh "__ff" in
let ivarmap := fresh "__varmap" in