From f9d3a620f4c6d920465f3b84bd2f3441c7cb07bc Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 11 Mar 2025 16:27:31 -0400 Subject: [PATCH] Remove itauto dependency as it introduces weird axioms --- theories/algorithmic.v | 5 ++--- theories/fp_red.v | 14 +++++++------- theories/logrel.v | 16 ++++++++-------- 3 files changed, 17 insertions(+), 18 deletions(-) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index d9711e1..184872d 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -5,7 +5,6 @@ Require Import ssreflect ssrbool. Require Import Psatz. From stdpp Require Import relations (rtc(..), nsteps(..)). Require Import Coq.Logic.FunctionalExtensionality. -Require Import Cdcl.Itauto. Module HRed. Lemma ToRRed (a b : PTm) : HRed.R a b -> RRed.R a b. @@ -98,7 +97,7 @@ Proof. - move => u v hC /andP [h0 h1] /synsub_to_usub ?. exfalso. suff : SNe (PApp u v) by hauto l:on use:Sub.bind_sne_noconf. - eapply ne_nf_embed => //=. itauto. + eapply ne_nf_embed => //=. sfirstorder b:on. - move => p0 p1 hC h ?. exfalso. have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity. hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv. @@ -199,7 +198,7 @@ Proof. - move => u v hC /andP [h0 h1] /synsub_to_usub ?. exfalso. suff : SNe (PApp u v) by hauto l:on use:Sub.sne_bind_noconf. - eapply ne_nf_embed => //=. itauto. + eapply ne_nf_embed => //=. sfirstorder b:on. - move => p0 p1 hC h ?. exfalso. have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity. hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv. diff --git a/theories/fp_red.v b/theories/fp_red.v index 9d8718b..382f25b 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -10,7 +10,7 @@ From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn). From Hammer Require Import Tactics. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common. Require Import Btauto. -Require Import Cdcl.Itauto. + Ltac2 spec_refl () := List.iter @@ -2575,7 +2575,7 @@ Module LoReds. ~~ ishf a. Proof. move : hf_preservation. repeat move/[apply]. - case : a; case : b => //=; itauto. + case : a; case : b => //=; sfirstorder b:on. Qed. #[local]Ltac solve_s_rec := @@ -2633,7 +2633,7 @@ Module LoReds. rtc LoRed.R (PSuc a0) (PSuc a1). Proof. solve_s. Qed. - Local Ltac triv := simpl in *; itauto. + Local Ltac triv := simpl in *; sfirstorder b:on. Lemma FromSN_mutual : (forall (a : PTm) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\ @@ -3048,7 +3048,7 @@ Module DJoin. have {h0 h1 h2 h3} : isbind c /\ isuniv c by hauto l:on use:REReds.bind_preservation, REReds.univ_preservation. - case : c => //=; itauto. + case : c => //=; sfirstorder b:on. Qed. Lemma hne_univ_noconf (a b : PTm) : @@ -3078,7 +3078,7 @@ Module DJoin. Proof. move => [c [h0 h1]] h2 h3. have : ishne c /\ isnat c by sfirstorder use:REReds.hne_preservation, REReds.nat_preservation. - clear. case : c => //=; itauto. + clear. case : c => //=; sfirstorder b:on. Qed. Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 : @@ -3594,7 +3594,7 @@ Module Sub. hauto l:on use:REReds.bind_preservation, REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation. move : h2 h3. clear. - case : c => //=; itauto. + case : c => //=; sfirstorder b:on. Qed. Lemma univ_bind_noconf (a b : PTm) : @@ -3605,7 +3605,7 @@ Module Sub. hauto l:on use:REReds.bind_preservation, REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation. move : h2 h3. clear. - case : c => //=; itauto. + case : c => //=; sfirstorder b:on. Qed. Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 : diff --git a/theories/logrel.v b/theories/logrel.v index a479f81..d4b4bd9 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -6,7 +6,7 @@ Require Import ssreflect ssrbool. Require Import Logic.PropExtensionality (propositional_extensionality). From stdpp Require Import relations (rtc(..), rtc_subrel). Import Psatz. -Require Import Cdcl.Itauto. + Definition ProdSpace (PA : PTm -> Prop) (PF : PTm -> (PTm -> Prop) -> Prop) b : Prop := @@ -355,7 +355,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : SNe H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto. + suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. move : hA hAB. clear. hauto lq:on db:noconf. move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst. tauto. @@ -365,7 +365,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : SNe H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto. + suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. move : hAB hA h0. clear. hauto lq:on db:noconf. move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst. tauto. @@ -375,7 +375,7 @@ Proof. have {hU} {}h : Sub.R (PBind p A B) H by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have{h0} : isbind H. - suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto. + suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. have : isbind (PBind p A B) by scongruence. move : h. clear. hauto l:on db:noconf. case : H h1 h => //=. @@ -394,7 +394,7 @@ Proof. have {hU} {}h : Sub.R H (PBind p A B) by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have{h0} : isbind H. - suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto. + suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. have : isbind (PBind p A B) by scongruence. move : h. clear. move : (PBind p A B). hauto lq:on db:noconf. case : H h1 h => //=. @@ -413,7 +413,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R PNat H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : isnat H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto. + suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on. have : @isnat PNat by simpl. move : h0 hAB. clear. qauto l:on db:noconf. case : H h1 hAB h0 => //=. @@ -424,7 +424,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R H PNat by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : isnat H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto. + suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on. have : @isnat PNat by simpl. move : h0 hAB. clear. qauto l:on db:noconf. case : H h1 hAB h0 => //=. @@ -1058,7 +1058,7 @@ Definition Γ_sub' Γ Δ := forall ρ, ρ_ok Δ ρ -> ρ_ok Γ ρ. Definition Γ_eq' Γ Δ := forall ρ, ρ_ok Δ ρ <-> ρ_ok Γ ρ. Lemma Γ_sub'_refl Γ : Γ_sub' Γ Γ. - rewrite /Γ_sub'. itauto. Qed. + rewrite /Γ_sub'. sfirstorder b:on. Qed. Lemma Γ_sub'_cons Γ Δ A B i j : Sub.R B A ->