Questions tagged [prop]

A sort of definitionally proof-irrelevant propositions introduced in "Definitional Proof-Irrelevance without K" and implemented by Agda (as Prop) and Coq (as SProp).

Filter by
Sorted by
Tagged with
3 votes
1 answer
96 views

Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type?

In order to ensure soundness, and to keep axioms like proof irrelevance admissible, Coq has an "elimination restriction" on inductive types in Prop. ...
JoJoModding's user avatar
3 votes
3 answers
225 views

Pattern matching from `Prop` to `Type` in Lean

I'm a beginner in the world of proof assistants, and have been taking a look at Lean4 lately. I wanted to write a function like ...
Celso Bonutti's user avatar
1 vote
1 answer
69 views

Coq Induction on Hypothesis destroys the Hypothesis

I'm trying to prove something in coq I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the ...
asha soroushpoor's user avatar
6 votes
0 answers
147 views

How does the modality-based irrelevance compare to universe-based irrelevance (`Prop`)?

I understand proof irrelevance implementation as one of the two language features listed below: Prop as SProp in Coq or ...
ice1000's user avatar
  • 5,877
2 votes
0 answers
96 views

Is there a good demonstration of bidirectional type checking with strict Prop?

I've seen elaboration-zoo, pi-forall, Mini-TT, etc., all kinds of demonstrations of dependent type elaboration. However, none of them support Prop. I am interested ...
ice1000's user avatar
  • 5,877
5 votes
1 answer
184 views

Why can termination checker affect strict Prop in Agda?

In https://dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky's propositional resizing rule justifies the consistency of an ...
ice1000's user avatar
  • 5,877
5 votes
1 answer
151 views

Is 'subsingleton elimination' the same concept as 'function comprehension'?

I saw: subsingleton elimination from lean-forward, which, I so far understood as "eliminate a type in Prop to a type in whatever universe that we know has at ...
ice1000's user avatar
  • 5,877
4 votes
2 answers
167 views

Turning off some sProp checks

In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination: (1) Every non-forced argument must be in sProp. (2) The return types of ...
ionchy's user avatar
  • 906
10 votes
1 answer
314 views

How does Prop relate to h-prop and double negation?

I'm referring to these concepts: Prop in Agda and SProp in Coq, a "sort of definitionally proof-irrelevant propositions", and their squash type (and relatedly, the usual Prop in Coq); mere ...
James Martin's user avatar
  • 1,015
12 votes
3 answers
315 views

Why does it matter if canonicity holds for irrelevant types?

Suppose you were to add a non-constructive axiom which only applies to irrelevant types, such as the irrelevance axiom. To my understanding canonicity and strong normalization are defining features of ...
James Martin's user avatar
  • 1,015