yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Remove itauto dependency as it introduces weird axioms

Browse source
This commit is contained in:
Yiyun Liu 2025-03-11 16:27:31 -04:00
parent 8dbef3e29e
commit f9d3a620f4
3 changed files with 17 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

5
theories/algorithmic.v
View file

@ -5,7 +5,6 @@ Require Import ssreflect ssrbool.
Require Import Psatz. Require Import Psatz.
From stdpp Require Import relations (rtc(..), nsteps(..)). From stdpp Require Import relations (rtc(..), nsteps(..)).
Require Import Coq.Logic.FunctionalExtensionality. Require Import Coq.Logic.FunctionalExtensionality.
Require Import Cdcl.Itauto.
Module HRed. Module HRed.
Lemma ToRRed (a b : PTm) : HRed.R a b -> RRed.R a b. 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 ?. - move => u v hC /andP [h0 h1] /synsub_to_usub ?.
exfalso. exfalso.
suff : SNe (PApp u v) by hauto l:on use:Sub.bind_sne_noconf. 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. - move => p0 p1 hC h ?. exfalso.
have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity. 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. 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 ?. - move => u v hC /andP [h0 h1] /synsub_to_usub ?.
exfalso. exfalso.
suff : SNe (PApp u v) by hauto l:on use:Sub.sne_bind_noconf. 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. - move => p0 p1 hC h ?. exfalso.
have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity. 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. hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.

14
theories/fp_red.v
View file

@ -10,7 +10,7 @@ From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn).
From Hammer Require Import Tactics. From Hammer Require Import Tactics.
Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
Require Import Btauto. Require Import Btauto.
Require Import Cdcl.Itauto.
Ltac2 spec_refl () := Ltac2 spec_refl () :=
List.iter List.iter
@ -2575,7 +2575,7 @@ Module LoReds.
~~ ishf a. ~~ ishf a.
Proof. Proof.
move : hf_preservation. repeat move/[apply]. move : hf_preservation. repeat move/[apply].
case : a; case : b => //=; itauto. case : a; case : b => //=; sfirstorder b:on.
Qed. Qed.
#[local]Ltac solve_s_rec := #[local]Ltac solve_s_rec :=
@ -2633,7 +2633,7 @@ Module LoReds.
rtc LoRed.R (PSuc a0) (PSuc a1). rtc LoRed.R (PSuc a0) (PSuc a1).
Proof. solve_s. Qed. Proof. solve_s. Qed.
Local Ltac triv := simpl in *; itauto. Local Ltac triv := simpl in *; sfirstorder b:on.
Lemma FromSN_mutual : Lemma FromSN_mutual :
(forall (a : PTm) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\ (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 have {h0 h1 h2 h3} : isbind c /\ isuniv c by
hauto l:on use:REReds.bind_preservation, hauto l:on use:REReds.bind_preservation,
REReds.univ_preservation. REReds.univ_preservation.
case : c => //=; itauto. case : c => //=; sfirstorder b:on.
Qed. Qed.
Lemma hne_univ_noconf (a b : PTm) : Lemma hne_univ_noconf (a b : PTm) :
@ -3078,7 +3078,7 @@ Module DJoin.
Proof. Proof.
move => [c [h0 h1]] h2 h3. move => [c [h0 h1]] h2 h3.
have : ishne c /\ isnat c by sfirstorder use:REReds.hne_preservation, REReds.nat_preservation. 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. Qed.
Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 : Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 :
@ -3594,7 +3594,7 @@ Module Sub.
hauto l:on use:REReds.bind_preservation, hauto l:on use:REReds.bind_preservation,
REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation. REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
move : h2 h3. clear. move : h2 h3. clear.
case : c => //=; itauto. case : c => //=; sfirstorder b:on.
Qed. Qed.
Lemma univ_bind_noconf (a b : PTm) : Lemma univ_bind_noconf (a b : PTm) :
@ -3605,7 +3605,7 @@ Module Sub.
hauto l:on use:REReds.bind_preservation, hauto l:on use:REReds.bind_preservation,
REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation. REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
move : h2 h3. clear. move : h2 h3. clear.
case : c => //=; itauto. case : c => //=; sfirstorder b:on.
Qed. Qed.
Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 : Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 :

16
theories/logrel.v
View file

@ -6,7 +6,7 @@ Require Import ssreflect ssrbool.
Require Import Logic.PropExtensionality (propositional_extensionality). Require Import Logic.PropExtensionality (propositional_extensionality).
From stdpp Require Import relations (rtc(..), rtc_subrel). From stdpp Require Import relations (rtc(..), rtc_subrel).
Import Psatz. Import Psatz.
Require Import Cdcl.Itauto.
Definition ProdSpace (PA : PTm -> Prop) Definition ProdSpace (PA : PTm -> Prop)
(PF : PTm -> (PTm -> Prop) -> Prop) b : Prop := (PF : PTm -> (PTm -> Prop) -> Prop) b : Prop :=
@ -355,7 +355,7 @@ Proof.
move => [H [/DJoin.FromRedSNs h [h1 h0]]]. 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 {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have {}h0 : SNe H. 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 : hA hAB. clear. hauto lq:on db:noconf.
move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst. move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
tauto. tauto.
@ -365,7 +365,7 @@ Proof.
move => [H [/DJoin.FromRedSNs h [h1 h0]]]. 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 {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have {}h0 : SNe H. 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 : hAB hA h0. clear. hauto lq:on db:noconf.
move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst. move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
tauto. tauto.
@ -375,7 +375,7 @@ Proof.
have {hU} {}h : Sub.R (PBind p A B) H 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. by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have{h0} : isbind H. 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. have : isbind (PBind p A B) by scongruence.
move : h. clear. hauto l:on db:noconf. move : h. clear. hauto l:on db:noconf.
case : H h1 h => //=. case : H h1 h => //=.
@ -394,7 +394,7 @@ Proof.
have {hU} {}h : Sub.R H (PBind p A B) 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. by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have{h0} : isbind H. 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. have : isbind (PBind p A B) by scongruence.
move : h. clear. move : (PBind p A B). hauto lq:on db:noconf. move : h. clear. move : (PBind p A B). hauto lq:on db:noconf.
case : H h1 h => //=. case : H h1 h => //=.
@ -413,7 +413,7 @@ Proof.
move => [H [/DJoin.FromRedSNs h [h1 h0]]]. 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 {h}{}hAB : Sub.R PNat H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have {}h0 : isnat H. 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. have : @isnat PNat by simpl.
move : h0 hAB. clear. qauto l:on db:noconf. move : h0 hAB. clear. qauto l:on db:noconf.
case : H h1 hAB h0 => //=. case : H h1 hAB h0 => //=.
@ -424,7 +424,7 @@ Proof.
move => [H [/DJoin.FromRedSNs h [h1 h0]]]. 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 {h}{}hAB : Sub.R H PNat by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have {}h0 : isnat H. 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. have : @isnat PNat by simpl.
move : h0 hAB. clear. qauto l:on db:noconf. move : h0 hAB. clear. qauto l:on db:noconf.
case : H h1 hAB h0 => //=. case : H h1 hAB h0 => //=.
@ -1058,7 +1058,7 @@ Definition Γ_sub' Γ Δ := forall ρ, ρ_ok Δ ρ -> ρ_ok Γ ρ.
Definition Γ_eq' Γ Δ := forall ρ, ρ_ok Δ ρ <-> ρ_ok Γ ρ. Definition Γ_eq' Γ Δ := forall ρ, ρ_ok Δ ρ <-> ρ_ok Γ ρ.
Lemma Γ_sub'_refl Γ : Γ_sub' Γ Γ. Lemma Γ_sub'_refl Γ : Γ_sub' Γ Γ.
rewrite /Γ_sub'. itauto. Qed. rewrite /Γ_sub'. sfirstorder b:on. Qed.
Lemma Γ_sub'_cons Γ Δ A B i j : Lemma Γ_sub'_cons Γ Δ A B i j :
Sub.R B A -> Sub.R B A ->