Skip to content

Port matching-logic library toward Rocq dev #455

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.

Sign up for GitHub

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

Draft
JasonGross wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

Port matching-logic library toward Rocq dev #455

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
182bc3d
Port matching-logic library toward Rocq dev
JasonGross Jul 28, 2026
c3c5819
Advance Matching Logic build with Rocq dev
JasonGross Jul 28, 2026
7db02db
Adapt core proofs to Rocq dev
JasonGross Jul 28, 2026
856b5e9
Port fixpoint reasoning to Rocq dev
JasonGross Jul 28, 2026
75721ba
Keep aborted model experiments compatible with Rocq dev
JasonGross Jul 28, 2026
c0089e2
Exclude obsolete generated model experiment
JasonGross Jul 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions matching-logic/dune-project
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
(lang dune 2.5)
(using coq 0.2)
(name coq-matching-logic)
(package
(name coq-matching-logic))
46 changes: 26 additions & 20 deletions matching-logic/src/BasicProofSystemLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,17 +233,18 @@ Proof.
++ eapply MP.
** eapply MP.
--- apply(P2 _ A B C ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
--- unshelve (eapply(P1 _ _ (A ---> B ---> C) _ _)); wf_auto2.
** apply P2; wf_auto2.
--- unshelve (eapply(P1 _ _ (A ---> B ---> C) _ _)).
all: solve [wf_auto2].
** apply P2. all: solve [wf_auto2].
-- eapply MP.
++ apply t1.
++ apply(P2 _ ABC ((A ---> B) ---> (A ---> C)) (B ---> (A ---> B) ---> (A ---> C)) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
* eapply MP.
-- eapply MP.
++ apply(P2 _ B (A ---> B) (A ---> C) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
++ apply(P1 _ _ ABC); wf_auto2.
-- apply P2; wf_auto2.
+ apply P2; wf_auto2.
++ apply(P1 _ _ ABC). all: solve [wf_auto2].
-- apply P2. all: solve [wf_auto2].
+ apply P2. all: solve [wf_auto2].
Defined.

Lemma reorder_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
Expand All @@ -269,12 +270,13 @@ Proof.
intros WFA WFB WFC.
apply reorder_meta;[wf_auto2|wf_auto2|wf_auto2|].
eapply MP.
- apply(P1 _ (B ---> C) A); wf_auto2.
- apply(P1 _ (B ---> C) A). all: solve [wf_auto2].
- eapply MP.
+ eapply MP.
* apply (P2 _ A B C); wf_auto2.
* apply (P1 _ ((A ---> B ---> C) ---> (A ---> B) ---> A ---> C) (B ---> C)); wf_auto2.
+ apply P2; wf_auto2.
* apply (P2 _ A B C). all: solve [wf_auto2].
* apply (P1 _ ((A ---> B ---> C) ---> (A ---> B) ---> A ---> C) (B ---> C)).
all: solve [wf_auto2].
+ apply P2. all: solve [wf_auto2].
Defined.

Lemma syllogism_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
Expand All @@ -292,7 +294,7 @@ Proof.
+ exact H3.
+ apply reorder_meta;[wf_auto2|wf_auto2|wf_auto2|].
apply useBasicReasoning.
apply syllogism; wf_auto2.
apply syllogism. all: solve [wf_auto2].
Defined.

Lemma modus_ponens {Σ : Signature} (Γ : Theory) (A B : Pattern) :
Expand All @@ -309,7 +311,7 @@ Proof.
* apply (A_impl_A _ (A ---> B) ltac:(wf_auto2)).
* eapply (P2 _ (A ---> B) A B ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
+ apply reorder_meta;[wf_auto2|wf_auto2|wf_auto2|].
apply syllogism; wf_auto2.
apply syllogism. all: solve [wf_auto2].
Defined.

Lemma not_not_intro {Σ : Signature} (Γ : Theory) (A : Pattern) :
Expand Down Expand Up @@ -414,15 +416,17 @@ Proof.
-- eapply MP.
++ exact H0.
++ apply useBasicReasoning.
eapply (P1 _ (C ---> D) B _ _).
eapply (P1 _ (C ---> D) B
ltac:(wf_auto2) ltac:(wf_auto2)).
-- apply useBasicReasoning.
eapply (P2 _ B C D _ _ _).
eapply (P2 _ B C D
ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
* apply useBasicReasoning.
eapply (P1 _ ((B ---> C) ---> B ---> D) A _ _).
eapply (P1 _ ((B ---> C) ---> B ---> D) A
ltac:(wf_auto2) ltac:(wf_auto2)).
+ apply useBasicReasoning.
eapply (P2 _ A (B ---> C) (B ---> D) _ _ _).
Unshelve.
all: wf_auto2.
eapply (P2 _ A (B ---> C) (B ---> D)
ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
Defined.

Lemma bot_elim {Σ : Signature} (Γ : Theory) (A : Pattern) :
Expand Down Expand Up @@ -535,9 +539,11 @@ Lemma double_neg_elim {Σ : Signature} (Γ : Theory) (A B : Pattern) :
Proof.
intros WFA WFB.
eapply syllogism_meta.
5: apply P4.
4: apply P4.
all: wf_auto2.
- wf_auto2.
- wf_auto2.
- wf_auto2.
- apply P4.
- apply P4.
Defined.

Lemma double_neg_elim_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
Expand Down
4 changes: 2 additions & 2 deletions matching-logic/src/Experimental/ProofModePattern.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,7 @@ Section sec.
simp PMPattern_size.
rewrite PMPattern_size_clause_2_PMPattern_size_vec_spec.
remember (vec_to_list args) as args'.
apply elem_of_list_lookup_1 in pf.
apply list_elem_of_lookup_1 in pf.
destruct pf as [i Hi].
pose proof (Hargs := take_drop_middle args' i p Hi).
subst.
Expand Down Expand Up @@ -1271,4 +1271,4 @@ Section sec.

End examples.

End sec.
End sec.
43 changes: 2 additions & 41 deletions matching-logic/src/Experimental/Test.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ Require Import

Import MatchingLogic.Logic.Notations.
Import MatchingLogic.Semantics.Notations.
Import MatchingLogic.Semantics.

Open Scope ml_scope.

Expand Down Expand Up @@ -121,50 +122,10 @@ Section natbool.
Definition get_signature {Σ : Signature} (m : @Model Σ) : Signature := Σ.

Instance def_syntax : @Definedness_Syntax.Syntax (get_signature DefinedNatBoolModel) := {
inj _ := inr ();
sym_inj _ := inr ();
}.

Goal DefinedNatBoolModel ⊨ᵀ Definedness_Syntax.theory.
Proof.
unfold theory, named_axioms, theory_of_NamedAxioms. simpl.
unfold satisfies_theory. intros. apply elem_of_PropSet in H.
destruct H, x. subst. cbn. unfold satisfies_model. intros.
unfold patt_defined, p_x, ev_x. simp eval.
unfold app_ext. simpl. unshelve eapply leibniz_equiv.
exact (@propset_leibniz_equiv _ DefinedNatBoolModel).
eapply set_equiv. intros. split; intros. set_solver.
rewrite elem_of_PropSet.
exists (inr ()), (evar_valuation ρ (evar_fresh [])).
split. set_solver. split. set_solver.
case_match. set_solver.
(* This condition is unsolvable. It comes from
* Mext def -> obligation 1 -> case 4 and
* PlainDefinedness def -> app_interp.
* These definitions both seen sensible on their own.
* Use the second models app_interp if both elements are
* from the second model, then wrap it in inr. Also
* def $ def is full set (right?). However, when we combine
* these, we get something wrong. I suspect this is because
* def $ def needs to be full set even AFTER gluing the models,
* and not inr <$> full set. We could take as extra params in
* ModelCombiners two functions that specifiy these special
* behaviours, maybe even functions returning options,
* so we retain the default behaviour of delegating to
* the sets underlying app_interp. This raises two questions:
* - Are there any other cases where this is needed or is this
* special to definedness? Should definedness be treated as
* special and we don't need this change elsewhere?
* ∙ PB: Yes, potentially generic datatypes would raise this issue too.
For example, lists, maps, sets. Depending on the element's sort
you might need to extend the behaviour of list/set/etc. symbols.
* - If we override the models original app_interp, do we not
* lose any reasoning we did about the original one? Is there
* a way to retain the proofs and allow special behaviour?
* ∙ PB: This is a main question. I think, you can only retain the original
behaviour, if you override (or rather, extend) the behaviour in a
correct way. For example, in case of definedness, you extend its
interpretation in M₂ to full.
*)
Abort.
End natbool.

Expand Down
84 changes: 20 additions & 64 deletions matching-logic/src/FixpointReasoning.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,7 @@ Section with_signature.
Qed.

Definition is_witnessing_sequence_old (m : Domain M) (l : list (Domain M)) :=
(last l = Some m) /\
(list.last l = Some m) /\
(match l with
| [] => False
| m₀::ms => (m₀ ∈ @eval Σ M ρ base)
Expand All @@ -241,7 +241,7 @@ Section with_signature.
(* This sequence is the reversed version from the informal introduction in line 139
For example, for Nat model elements, the witnessing sequence for 5 is [5,4,3,2,1,0] *)
Definition is_witnessing_sequence (m : Domain M) (l : list (Domain M)) :=
(∃ lst, last l = Some lst /\ lst ∈ @eval Σ M ρ base)
(∃ lst, list.last l = Some lst /\ lst ∈ @eval Σ M ρ base)
/\
hd_error l = Some m
/\
Expand Down Expand Up @@ -421,49 +421,6 @@ Section with_signature.
(* TODO: would this be easier to use/prove/understand to
have `m' ∈ app_ext (eval ρ step) {[m]}` instead? *)
) <-> (is_witnessing_sequence m' (m'::l) /\ l ≠ []).
Proof.
split.
- intros [[[lst [Hlst Hbase] ] [Hhd Hwit] ] [step' [Hstep' Hm'] ] ].
split.
2: { destruct l. simpl in Hhd. inversion Hhd. discriminate. }
move: m Hhd m' step' Hm' Hstep'.
induction l; intros m Hhd m' step' Hm' Hstep'.
+ simpl in Hhd. inversion Hhd.
+ simpl in Hhd. inversion Hhd. subst a. clear Hhd.
unfold is_witnessing_sequence.
destruct l.
{ simpl in Hlst. inversion Hlst. subst m. clear Hlst.
split.
{ exists lst. simpl. split. reflexivity. apply Hbase. }
simpl. split. reflexivity. apply Forall_cons.
split. exists step'. exists lst. split.
apply Hstep'. split. constructor. apply Hm'.
apply Forall_nil. exact I.
}
split.
{ exists lst. split. simpl. simpl in Hlst. apply Hlst. apply Hbase. }
split.
{ reflexivity. }
simpl in Hwit. simpl.
apply Forall_cons.
simpl in IHl. simpl in Hlst.
specialize (IHl Hlst).
inversion Hwit. subst. clear Hwit.
specialize (IHl H2). clear Hlst H2.
split.
{ exists step'. exists m. split. apply Hstep'. split. constructor. apply Hm'. }
apply Forall_cons.
split.
{ apply H1. }
specialize (IHl d erefl).
destruct H1 as [step'' [d'' [Hstep'' [Hd'' Hstep''d''] ] ] ].
inversion Hd''. subst d''. clear Hd''.
specialize (IHl m step'' Hstep''d'' Hstep'').
unfold is_witnessing_sequence in IHl.
simpl in IHl.
destruct IHl as [_ [_ Hforall] ].
inversion Hforall. subst. apply H2.
-
Abort.


Expand All @@ -472,7 +429,7 @@ Section with_signature.
(is_witnessing_sequence_old m (x::l) /\
∃ step', (step' ∈ eval ρ step /\
m' ∈ app_interp _ step' m)) <->
(last (x::l) = Some m /\ is_witnessing_sequence_old m' ((x::l) ++ [m'])).
(list.last (x::l) = Some m /\ is_witnessing_sequence_old m' ((x::l) ++ [m'])).
Proof.
split.
-
Expand All @@ -487,7 +444,7 @@ Section with_signature.
{ apply Hwit2. }

destruct l.
{ simpl. apply Forall_cons. split. 2: { apply Forall_nil. exact I. }
{ simpl. apply Forall_cons. 2: { apply Forall_nil. }
exists step'. exists x. split.
{ apply Hstep'. }
split.
Expand All @@ -496,19 +453,18 @@ Section with_signature.
}
simpl.
apply Forall_cons.
simpl in Hwit3. inversion Hwit3. subst. clear Hwit3.
rename H1 into Hd. rename H2 into Hwit.
split.
{ apply Hd. } clear Hd.
simpl in Hwit3.
{ apply (Forall_inv Hwit3). }

pose proof (Forall_inv_tail Hwit3) as Hwit.
clear Hwit3.
move: d Hwit1 Hwit.
induction l.
+ intros D Hm _.
simpl. simpl in Hm. inversion Hm. subst.
clear Hm.
apply Forall_cons.
split.
2: { apply Forall_nil. exact I. }
2: { apply Forall_nil. }
exists step'. exists m. split.
{ apply Hstep'. }
split.
Expand All @@ -517,7 +473,6 @@ Section with_signature.
+ intros d Hlast Hwit. simpl.
inversion Hwit. subst.
apply Forall_cons.
split.
{ apply H1. }
apply IHl. simpl in Hlast. simpl. apply Hlast.
apply H2.
Expand Down Expand Up @@ -545,7 +500,7 @@ Section with_signature.
2: { simpl in Hlen. lia. }
simpl. simpl in Hall.
split.
{ apply Forall_nil. exact I. }
{ apply Forall_nil. }
inversion Hall. subst. clear Hall. clear H2.
destruct H1 as [step' [m'' [Hstep' [Hm'm'' Hstep'm''] ] ] ].
inversion Hm'm''. subst. clear Hm'm''.
Expand All @@ -560,7 +515,7 @@ Section with_signature.
clear H2.
simpl.
split.
{ apply Forall_nil. exact I. }
{ apply Forall_nil. }
destruct H1 as [step' Hstep'].
exists step'.
destruct Hstep' as [m'' [Hstep' [Hmm'' Hm''] ] ].
Expand All @@ -571,14 +526,16 @@ Section with_signature.
}
simpl in Hall. simpl in IHlen. simpl in Hlast.
inversion Hall. subst. clear Hall.
specialize (IHlen x' l' Hlast H2).
assert (Hlen' : length l' <= len) by (simpl in Hlen; lia).
specialize (IHlen x' l' Hlast H2 Hlen').
simpl.
rewrite Forall_cons.
apply and_assoc.
destruct IHlen as [IHfor IHex].
split.
{ apply H1. }
apply IHlen.
simpl in Hlen. lia.
{ apply Forall_cons.
{ apply H1. }
apply IHfor.
}
apply IHex.
Qed.

Definition witnessed_elements_old : propset (Domain M) :=
Expand Down Expand Up @@ -720,7 +677,6 @@ Section with_signature.
split.
{ apply Hd. }
apply Forall_nil.
exact I.
}
apply Hm.
}
Expand Down Expand Up @@ -776,7 +732,7 @@ Section with_signature.
simpl in P.
rewrite -H2 in P.

assert (Hm : (match l with [] => Some d1 | _ :: _ => last l end ) = Some mprev).
assert (Hm : (match l with [] => Some d1 | _ :: _ => list.last l end ) = Some mprev).
{
clear P Heqrev H1 H3 H4 mp.
destruct l.
Expand Down
Loading